Library GeoCoq.Elements.OriginalProofs.lemma_angleorderrespectscongruence2

Require Export GeoCoq.Elements.OriginalProofs.lemma_equalanglestransitive.

Section Euclid.

Context `{Ax:euclidean_neutral}.

Lemma lemma_angleorderrespectscongruence2 :
    A B C D E F a b c,
   LtA A B C D E F CongA a b c A B C
   LtA a b c D E F.
Proof.
intros.
let Tf:=fresh in
assert (Tf: P Q R, (BetS P Q R Out E D P Out E F R CongA A B C D E Q)) by (conclude_def LtA );destruct Tf as [P[Q[R]]];spliter.
assert (CongA a b c D E Q) by (conclude lemma_equalanglestransitive).
assert (LtA a b c D E F) by (conclude_def LtA ).
close.
Qed.

End Euclid.