proposition: Lemma lemma_tworays : forall A B C, Out A B C -> Out B A C -> BetS A C B.
proof: Proof. intros. assert ((BetS A C B \/ eq B C \/ BetS A B C)) by (conclude lemma_ray1). assert ((BetS B C A \/ eq A C \/ BetS B A C)) by (conclude lemma_ray1). assert (BetS A C B). by cases on (BetS A C B \/ eq B C \/ BetS A B C). { close. } { assert (~ ~ BetS A C B). { intro. assert (neq B C) by (conclude lemma_raystrict). contradict. } close. } { assert (BetS A C B). by cases on (BetS B C A \/ eq A C \/ BetS B A C). { assert (BetS A C B) by (conclude axiom_betweennesssymmetry). close. } { assert (~ ~ BetS A C B). { intro. assert (neq A C) by (conclude lemma_raystrict). contradict. } close. } { assert (~ ~ BetS A C B). { intro. assert (BetS A B A) by (conclude axiom_innertransitivity). assert (~ BetS A B A) by (conclude axiom_betweennessidentity). contradict. } close. } close. } close. Qed.
imports: GeoCoq.Elements.OriginalProofs.lemma_ray1 GeoCoq.Elements.OriginalProofs.lemma_raystrict