proposition: Lemma euclid : ~ euclidP (@Point R 1) (@bet' R 1).
proof: Proof. move=> HP; apply euclid_fails; cut (tarski_s_parallel_postulate). rewrite /tarski_s_parallel_postulate; move=> HT A B C D T H1 H2 HBD HDC HNCol. apply HT with D; auto; intro; subst; apply HNCol; right; right. apply bet_symmetry, H2. cut (proclus_postulate); [|rewrite /proclus_postulate]. apply equivalent_postulates_without_decidability_of_intersection_of_lines_bis; simpl; try tauto. intros A B C D P Q HPar HC HNC HCop; apply HP with A B; [clear HC HNC HCop|intuition..]. destruct HPar as [[HCop HNI]|HParC]; [left|right; intuition]. split; [intro; treat_equalities; apply HNI; exists C; Col|]. split; [intro; treat_equalities; apply HNI; exists A; Col|]. split; [intuition|intros [X [? ?]]; apply HNI; exists X; Col]. 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