Require Export GeoCoq.Elements.OriginalProofs.lemma_extension.

Section Euclid.

Context `{Ax:euclidean_neutral_ruler_compass}.

Lemma lemma_layoff : 
   forall A B C D, 
   neq A B -> neq C D ->
   exists X, Out A B X /\ Cong A X C D.
Proof.
(* Goal: forall (A B C D : @Point Ax0) (_ : @neq Ax0 A B) (_ : @neq Ax0 C D), @ex (@Point Ax0) (fun X : @Point Ax0 => and (@Out Ax0 A B X) (@Cong Ax0 A X C D)) *)
intros.
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@Out Ax0 A B X) (@Cong Ax0 A X C D)) *)
assert (~ eq B A).
(* Goal: not (@eq Ax0 B A) *)
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@Out Ax0 A B X) (@Cong Ax0 A X C D)) *)
 {
(* Goal: not (@eq Ax0 B A) *)
 intro.
(* Goal: False *)
 assert (eq A B) by (conclude lemma_equalitysymmetric).
(* Goal: False *)
 contradict.
 }
let Tf:=fresh in
assert (Tf:exists E, (BetS B A E /\ Cong A E C D)) by (conclude lemma_extension);destruct Tf as [E];spliter.
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@Out Ax0 A B X) (@Cong Ax0 A X C D)) *)
assert (BetS E A B) by (conclude axiom_betweennesssymmetry).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@Out Ax0 A B X) (@Cong Ax0 A X C D)) *)
assert (neq E A) by (forward_using lemma_betweennotequal).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@Out Ax0 A B X) (@Cong Ax0 A X C D)) *)
assert (BetS E A B) by (conclude axiom_betweennesssymmetry).
let Tf:=fresh in
assert (Tf:exists P, (BetS E A P /\ Cong A P C D)) by (conclude lemma_extension);destruct Tf as [P];spliter.
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@Out Ax0 A B X) (@Cong Ax0 A X C D)) *)
assert (Out A B P) by (conclude_def Out ).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@Out Ax0 A B X) (@Cong Ax0 A X C D)) *)
close.
Qed.

End Euclid.


