Require Export GeoCoq.Elements.OriginalProofs.lemma_congruencetransitive.

Section Euclid.

Context `{Ax1:euclidean_neutral}.

Lemma lemma_lessthancongruence2 : 
   forall A B C D E F, 
   Lt A B C D -> Cong A B E F ->
   Lt E F C D.
Proof.
(* Goal: forall (A B C D E F : @Point Ax1) (_ : @Lt Ax1 A B C D) (_ : @Cong Ax1 A B E F), @Lt Ax1 E F C D *)
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 Ax1 E F C D *)
assert (Cong C G E F) by (conclude lemma_congruencetransitive).
(* Goal: @Lt Ax1 E F C D *)
assert (Lt E F C D) by (conclude_def Lt ).
(* Goal: @Lt Ax1 E F C D *)
close.
Qed.

End Euclid.


