Require Export GeoCoq.Elements.OriginalProofs.lemma_extension.
Require Export GeoCoq.Elements.OriginalProofs.lemma_betweennesspreserved. 

Section Euclid.

Context `{Ax1:euclidean_neutral_ruler_compass}.

Lemma lemma_lessthancongruence : 
   forall A B C D E F, 
   Lt A B C D -> Cong C D E F ->
   Lt A B E F.
Proof.
(* Goal: forall (A B C D E F : @Point Ax) (_ : @Lt Ax A B C D) (_ : @Cong Ax C D E F), @Lt Ax A B E F *)
intros.
let Tf:=fresh in
assert (Tf:exists G, (BetS C G D /\ Cong C G A B)) by (conclude_def Lt );destruct Tf as [G];spliter.
(* Goal: @Lt Ax A B E F *)
assert (neq C D) by (forward_using lemma_betweennotequal).
(* Goal: @Lt Ax A B E F *)
assert (neq E F) by (conclude axiom_nocollapse).
(* Goal: @Lt Ax A B E F *)
assert (~ eq F E).
(* Goal: not (@eq Ax D C) *)
(* Goal: @Lt Ax A B E F *)
 {
(* Goal: not (@eq Ax D C) *)
 intro.
(* Goal: False *)
 assert (eq E F) by (conclude lemma_equalitysymmetric).
(* Goal: False *)
 contradict.
 }
let Tf:=fresh in
assert (Tf:exists P, (BetS F E P /\ Cong E P F E)) by (conclude lemma_extension);destruct Tf as [P];spliter.
(* Goal: @Lt Ax A B E F *)
assert (BetS P E F) by (conclude axiom_betweennesssymmetry).
(* Goal: @Lt Ax A B E F *)
assert (neq P E) by (forward_using lemma_betweennotequal).
(* Goal: @Lt Ax A B E F *)
assert (neq C G) by (forward_using lemma_betweennotequal).
(* Goal: @Lt Ax A B E F *)
assert (neq A B) by (conclude axiom_nocollapse).
rename_H H;let Tf:=fresh in
assert (Tf:exists H, (BetS P E H /\ Cong E H A B)) by (conclude lemma_extension);destruct Tf as [H];spliter.
(* Goal: @Lt Ax A B E F *)
assert (~ eq D C).
(* Goal: not (@eq Ax D C) *)
(* Goal: @Lt Ax A B E F *)
 {
(* Goal: not (@eq Ax D C) *)
 intro.
(* Goal: False *)
 assert (BetS C G C) by (conclude cn_equalitysub).
(* Goal: False *)
 assert (~ BetS C G C) by (conclude axiom_betweennessidentity).
(* Goal: False *)
 contradict.
 }
(* Goal: @Lt Ax A B E F *)
assert (neq P E) by (forward_using lemma_betweennotequal).
(* Goal: @Lt Ax A B E F *)
assert (neq E P) by (conclude lemma_inequalitysymmetric).
let Tf:=fresh in
assert (Tf:exists Q, (BetS D C Q /\ Cong C Q E P)) by (conclude lemma_extension);destruct Tf as [Q];spliter.
(* Goal: @Lt Ax A B E F *)
assert (BetS Q C D) by (conclude axiom_betweennesssymmetry).
(* Goal: @Lt Ax A B E F *)
assert (Cong Q C C Q) by (conclude cn_equalityreverse).
(* Goal: @Lt Ax A B E F *)
assert (Cong Q C E P) by (conclude lemma_congruencetransitive).
(* Goal: @Lt Ax A B E F *)
assert (Cong E P P E) by (conclude cn_equalityreverse).
(* Goal: @Lt Ax A B E F *)
assert (Cong Q C P E) by (conclude lemma_congruencetransitive).
(* Goal: @Lt Ax A B E F *)
assert (Cong Q D P F) by (conclude cn_sumofparts).
(* Goal: @Lt Ax A B E F *)
assert (Cong A B E H) by (conclude lemma_congruencesymmetric).
(* Goal: @Lt Ax A B E F *)
assert (Cong C G E H) by (conclude lemma_congruencetransitive).
(* Goal: @Lt Ax A B E F *)
assert (BetS Q C G) by (conclude axiom_innertransitivity).
(* Goal: @Lt Ax A B E F *)
assert (Cong D G F H) by (conclude axiom_5_line).
(* Goal: @Lt Ax A B E F *)
assert (Cong G D H F) by (forward_using lemma_doublereverse).
(* Goal: @Lt Ax A B E F *)
assert (BetS E H F) by (conclude lemma_betweennesspreserved).
(* Goal: @Lt Ax A B E F *)
assert (Lt A B E F) by (conclude_def Lt ).
(* Goal: @Lt Ax A B E F *)
close.
Qed.

End Euclid.


