Require Export GeoCoq.Elements.OriginalProofs.lemma_outerconnectivity.

Section Euclid.

Context `{Ax:euclidean_neutral_ruler_compass}.


Lemma lemma_ray3 : 
   forall B C D V, 
   Out B C D -> Out B C V ->
   Out B D V.
Proof.
(* Goal: forall (B C D V : @Point Ax0) (_ : @Out Ax0 B C D) (_ : @Out Ax0 B C V), @Out Ax0 B D V *)
intros.
let Tf:=fresh in
assert (Tf:exists E, (BetS E B D /\ BetS E B C)) by (conclude_def Out );destruct Tf as [E];spliter.
rename_H H;let Tf:=fresh in
assert (Tf:exists H, (BetS H B V /\ BetS H B C)) by (conclude_def Out );destruct Tf as [H];spliter.
(* Goal: @Out Ax0 B D V *)
assert (~ ~ BetS E B V).
(* Goal: not (@BetS Ax0 B H E) *)
(* Goal: False *)
 {
(* Goal: not (@BetS Ax0 B H E) *)
 intro.
(* Goal: False *)
 assert (~ BetS B E H).
(* Goal: not (@BetS Ax0 B H E) *)
(* Goal: False *)
  {
(* Goal: not (@BetS Ax0 B H E) *)
  intro.
(* Goal: False *)
  assert (BetS H E B) by (conclude axiom_betweennesssymmetry).
(* Goal: False *)
  assert (BetS E B V) by (conclude lemma_3_6a).
(* Goal: False *)
  contradict.
  }
(* Goal: False *)
 assert (~ BetS B H E).
(* Goal: not (@BetS Ax0 B H E) *)
(* Goal: False *)
  {
(* Goal: not (@BetS Ax0 B H E) *)
  intro.
(* Goal: False *)
  assert (BetS E H B) by (conclude axiom_betweennesssymmetry).
(* Goal: False *)
  assert (BetS E B V) by (conclude lemma_3_7a).
(* Goal: False *)
  contradict.
  }
(* Goal: False *)
 assert (BetS C B E) by (conclude axiom_betweennesssymmetry).
(* Goal: False *)
 assert (BetS C B H) by (conclude axiom_betweennesssymmetry).
(* Goal: False *)
 assert (eq H E) by (conclude lemma_outerconnectivity).
(* Goal: False *)
 assert (BetS E B V) by (conclude cn_equalitysub).
(* Goal: False *)
 contradict.
 }
(* Goal: @Out Ax0 B D V *)
assert (Out B D V) by (conclude_def Out ).
(* Goal: @Out Ax0 B D V *)
close.
Qed.

End Euclid.


