proposition: Lemma euclid_aux: (exists A B C D T : Point R 1, bet' A D T /\ bet' B D C /\ B <> D /\ D <> C /\ ~ (bet' A B C \/ bet' B C A \/ bet' C A B) /\ (forall X : Point R 1, bet' A B X -> (forall Y' : 'rV[R]_(2), bet (#A) (#C) Y' -> bet (#X) (#T) Y' -> (Y' *m Y'^T) 0 0 >= 1))) -> ~ (forall (A B C D T : (@Point R 1)), bet' A D T -> bet' B D C -> B <> D -> D <> C -> ~ (bet' A B C \/ bet' B C A \/ bet' C A B) -> exists X Y, bet' A B X /\ bet' A C Y /\ bet' X T Y).
proof: Proof. move => H H2. destruct H as [a [b [c [d [t [bADT [bBDC [bd_neq [dc_neq [ncol H]]]]]]]]]]. destruct (H2 a b c d t) as [x [y [bABX [bACY bXTY]]]] ; auto. clear H2. assert (Y_out_of_disk:= H x bABX (#y) bACY bXTY). destruct y as [yC Y_in_disk]. move:(le_lt_asym 1 ((yC *m yC^T) 0 0)). by rewrite Y_in_disk Y_out_of_disk. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun ssrnat eqtype choice seq) mathcomp(fintype finset finfun bigop order) mathcomp(ssralg ssrnum path generic_quotient matrix mxalgebra algC) mathcomp(zmodp) GeoCoq.Meta_theory.Models.POF_to_Tarski GeoCoq.Axioms.gupta_inspired_variant_axioms GeoCoq.Meta_theory.Models.tarski_to_gupta_inspired GeoCoq.Tarski_dev.Ch06_out_lines GeoCoq.Tarski_dev.Ch11_angles GeoCoq.Meta_theory.Parallel_postulates.parallel_postulates GeoCoq.Meta_theory.Counter_models.Planar.independence