Require Export GeoCoq.Elements.OriginalProofs.lemma_extension.

Section Euclid.
Context `{Ax:euclidean_neutral_ruler_compass}.
Lemma lemma_interior5 : 
   forall A B C D a b c d, 
   BetS A B C -> BetS a b c -> Cong A B a b -> Cong B C b c -> Cong A D a d -> Cong C D c d ->
   Cong B D b d.
Proof.
(* Goal: forall (A B C D a b c d : @Point Ax0) (_ : @BetS Ax0 A B C) (_ : @BetS Ax0 a b c) (_ : @Cong Ax0 A B a b) (_ : @Cong Ax0 B C b c) (_ : @Cong Ax0 A D a d) (_ : @Cong Ax0 C D c d), @Cong Ax0 B D b d *)
intros.
(* Goal: @Cong Ax0 B D b d *)
assert (neq B C) by (forward_using lemma_betweennotequal).
(* Goal: @Cong Ax0 B D b d *)
assert (neq A C) by (forward_using lemma_betweennotequal).
(* Goal: @Cong Ax0 B D b d *)
assert (~ eq C A).
(* Goal: not (@eq Ax0 c a) *)
(* Goal: @Cong Ax0 B D b d *)
 {
(* Goal: not (@eq Ax0 c a) *)
 intro.
(* Goal: False *)
 assert (eq A C) by (conclude lemma_equalitysymmetric).
(* Goal: False *)
 contradict.
 }
let Tf:=fresh in
assert (Tf:exists M, (BetS C A M /\ Cong A M B C)) by (conclude lemma_extension);destruct Tf as [M];spliter.
(* Goal: @Cong Ax0 B D b d *)
assert (Cong A M M A) by (conclude cn_equalityreverse).
(* Goal: @Cong Ax0 B D b d *)
assert (Cong M A A M) by (conclude lemma_congruencesymmetric).
(* Goal: @Cong Ax0 B D b d *)
assert (Cong M A B C) by (conclude lemma_congruencetransitive).
(* Goal: @Cong Ax0 B D b d *)
assert (neq b c) by (conclude axiom_nocollapse).
(* Goal: @Cong Ax0 B D b d *)
assert (neq a c) by (forward_using lemma_betweennotequal).
(* Goal: @Cong Ax0 B D b d *)
assert (~ eq c a).
(* Goal: not (@eq Ax0 c a) *)
(* Goal: @Cong Ax0 B D b d *)
 {
(* Goal: not (@eq Ax0 c a) *)
 intro.
(* Goal: False *)
 assert (eq a c) by (conclude lemma_equalitysymmetric).
(* Goal: False *)
 contradict.
 }
let Tf:=fresh in
assert (Tf:exists m, (BetS c a m /\ Cong a m b c)) by (conclude lemma_extension);destruct Tf as [m];spliter.
(* Goal: @Cong Ax0 B D b d *)
assert (Cong m a a m) by (conclude cn_equalityreverse).
(* Goal: @Cong Ax0 B D b d *)
assert (Cong m a b c) by (conclude lemma_congruencetransitive).
(* Goal: @Cong Ax0 B D b d *)
assert (Cong b c m a) by (conclude lemma_congruencesymmetric).
(* Goal: @Cong Ax0 B D b d *)
assert (Cong B C m a) by (conclude lemma_congruencetransitive).
(* Goal: @Cong Ax0 B D b d *)
assert (Cong M A m a) by (conclude lemma_congruencetransitive).
(* Goal: @Cong Ax0 B D b d *)
assert (Cong A C a c) by (conclude cn_sumofparts).
(* Goal: @Cong Ax0 B D b d *)
assert (Cong c a C A) by (forward_using lemma_doublereverse).
(* Goal: @Cong Ax0 B D b d *)
assert (Cong C A c a) by (conclude lemma_congruencesymmetric).
(* Goal: @Cong Ax0 B D b d *)
assert (BetS C B A) by (conclude axiom_betweennesssymmetry).
(* Goal: @Cong Ax0 B D b d *)
assert (BetS B A M) by (conclude lemma_3_6a).
(* Goal: @Cong Ax0 B D b d *)
assert (BetS c b a) by (conclude axiom_betweennesssymmetry).
(* Goal: @Cong Ax0 B D b d *)
assert (BetS b a m) by (conclude lemma_3_6a).
(* Goal: @Cong Ax0 B D b d *)
assert (Cong A M a m) by (forward_using lemma_congruenceflip).
(* Goal: @Cong Ax0 B D b d *)
assert (Cong D M d m) by (conclude axiom_5_line).
(* Goal: @Cong Ax0 B D b d *)
assert (BetS m a b) by (conclude axiom_betweennesssymmetry).
(* Goal: @Cong Ax0 B D b d *)
assert (BetS M A B) by (conclude axiom_betweennesssymmetry).
(* Goal: @Cong Ax0 B D b d *)
assert (Cong M D m d) by (forward_using lemma_congruenceflip).
(* Goal: @Cong Ax0 B D b d *)
assert (Cong D B d b) by (conclude axiom_5_line).
(* Goal: @Cong Ax0 B D b d *)
assert (Cong B D b d) by (forward_using lemma_congruenceflip).
(* Goal: @Cong Ax0 B D b d *)
close.
Qed.

End Euclid.

