proposition: Lemma euclid : euclidP (@Point 1 R) (@bet' 1 R).
proof: Proof. move => a b c d p q abcdP abpP abqP cdpqP. destruct (@proclus R 0 a b c d p q) as [y [pqyP cdyP]]; [..|exists y]; [move => {abpP abqP cdpqP}|intuition..]. elim abcdP; [move => {abcdP} [abcdP niP]; left|intuition]. split; [intuition| move => [x xP]; apply niP; exists x; intuition]. 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) mathcomp(zmodp) mathcomp(tuple fintype bigop) GeoCoq.Meta_theory.Models.POF_to_Tarski GeoCoq.Meta_theory.Counter_models.Planar.independence