Require Export GeoCoq.Elements.OriginalProofs.lemma_collinearright.

Section Euclid.

Context `{Ax:euclidean_neutral_ruler_compass}.

Lemma lemma_supplementofright : 
   forall A B C D F, 
   Supp A B C D F -> Per A B C ->
   Per F B D /\ Per D B F.
Proof.
(* Goal: forall (A B C D F : @Point Ax0) (_ : @Supp Ax0 A B C D F) (_ : @Per Ax0 A B C), and (@Per Ax0 F B D) (@Per Ax0 D B F) *)
intros.
(* Goal: and (@Per Ax0 F B D) (@Per Ax0 D B F) *)
assert ((Out B C D /\ BetS A B F)) by (conclude_def Supp ).
(* Goal: and (@Per Ax0 F B D) (@Per Ax0 D B F) *)
assert (Col A B F) by (conclude_def Col ).
(* Goal: and (@Per Ax0 F B D) (@Per Ax0 D B F) *)
assert (neq B F) by (forward_using lemma_betweennotequal).
(* Goal: and (@Per Ax0 F B D) (@Per Ax0 D B F) *)
assert (neq F B) by (conclude lemma_inequalitysymmetric).
(* Goal: and (@Per Ax0 F B D) (@Per Ax0 D B F) *)
assert (Per F B C) by (conclude lemma_collinearright).
(* Goal: and (@Per Ax0 F B D) (@Per Ax0 D B F) *)
assert (Per F B D) by (conclude lemma_8_3).
(* Goal: and (@Per Ax0 F B D) (@Per Ax0 D B F) *)
assert (Per D B F) by (conclude lemma_8_2).
(* Goal: and (@Per Ax0 F B D) (@Per Ax0 D B F) *)
close.
Qed.

End Euclid.


