Require Export GeoCoq.Elements.OriginalProofs.lemma_lessthancongruence2.
Require Export GeoCoq.Elements.OriginalProofs.lemma_lessthancongruence.

Section Euclid.

Context `{Ax1:euclidean_neutral_ruler_compass}.

Lemma lemma_together : 
   forall A B C D F G P Q a b c, 
   TG A a B b C c -> Cong D F A a -> Cong F G B b -> BetS D F G -> Cong P Q C c ->
   Lt P Q D G /\ neq A a /\ neq B b /\ neq C c.
Proof.
(* Goal: forall (A B C D F G P Q a b c : @Point Ax) (_ : @TG Ax A a B b C c) (_ : @Cong Ax D F A a) (_ : @Cong Ax F G B b) (_ : @BetS Ax D F G) (_ : @Cong Ax P Q C c), and (@Lt Ax P Q D G) (and (@neq Ax A a) (and (@neq Ax B b) (@neq Ax C c))) *)
intros.
let Tf:=fresh in
assert (Tf:exists R, (BetS A a R /\ Cong a R B b /\ Lt C c A R)) by (conclude_def TG );destruct Tf as [R];spliter.
(* Goal: and (@Lt Ax P Q D G) (and (@neq Ax A a) (and (@neq Ax B b) (@neq Ax C c))) *)
assert (Cong A a A a) by (conclude cn_congruencereflexive).
(* Goal: and (@Lt Ax P Q D G) (and (@neq Ax A a) (and (@neq Ax B b) (@neq Ax C c))) *)
assert (Cong B b a R) by (conclude lemma_congruencesymmetric).
(* Goal: and (@Lt Ax P Q D G) (and (@neq Ax A a) (and (@neq Ax B b) (@neq Ax C c))) *)
assert (Cong F G a R) by (conclude lemma_congruencetransitive).
(* Goal: and (@Lt Ax P Q D G) (and (@neq Ax A a) (and (@neq Ax B b) (@neq Ax C c))) *)
assert (Cong D G A R) by (conclude cn_sumofparts).
(* Goal: and (@Lt Ax P Q D G) (and (@neq Ax A a) (and (@neq Ax B b) (@neq Ax C c))) *)
assert (Cong A R D G) by (conclude lemma_congruencesymmetric).
(* Goal: and (@Lt Ax P Q D G) (and (@neq Ax A a) (and (@neq Ax B b) (@neq Ax C c))) *)
assert (Cong C c P Q) by (conclude lemma_congruencesymmetric).
(* Goal: and (@Lt Ax P Q D G) (and (@neq Ax A a) (and (@neq Ax B b) (@neq Ax C c))) *)
assert (Lt P Q A R) by (conclude lemma_lessthancongruence2).
(* Goal: and (@Lt Ax P Q D G) (and (@neq Ax A a) (and (@neq Ax B b) (@neq Ax C c))) *)
assert (Lt P Q D G) by (conclude lemma_lessthancongruence).
(* Goal: and (@Lt Ax P Q D G) (and (@neq Ax A a) (and (@neq Ax B b) (@neq Ax C c))) *)
assert (neq A a) by (forward_using lemma_betweennotequal).
(* Goal: and (@Lt Ax P Q D G) (and (@neq Ax A a) (and (@neq Ax B b) (@neq Ax C c))) *)
assert (neq a R) by (forward_using lemma_betweennotequal).
(* Goal: and (@Lt Ax P Q D G) (and (@neq Ax A a) (and (@neq Ax B b) (@neq Ax C c))) *)
assert (neq B b) by (conclude axiom_nocollapse).
let Tf:=fresh in
assert (Tf:exists S, (BetS A S R /\ Cong A S C c)) by (conclude_def Lt );destruct Tf as [S];spliter.
(* Goal: and (@Lt Ax P Q D G) (and (@neq Ax A a) (and (@neq Ax B b) (@neq Ax C c))) *)
assert (neq A S) by (forward_using lemma_betweennotequal).
(* Goal: and (@Lt Ax P Q D G) (and (@neq Ax A a) (and (@neq Ax B b) (@neq Ax C c))) *)
assert (neq C c) by (conclude axiom_nocollapse).
(* Goal: and (@Lt Ax P Q D G) (and (@neq Ax A a) (and (@neq Ax B b) (@neq Ax C c))) *)
close.
Qed.

End Euclid.


