proposition: Lemma coplanarP a b c d : coplanar a b c d <-> Coplanar (@Point R) (@bet' R) a b c d.
proof: Proof. split; move=> [x [[]|[[]|[]]]]; exists x; try solve [by left; split; apply colP]; try solve [by right; left; split; apply colP]; by right; right ; split; apply colP. 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) GeoCoq.Axioms.gupta_inspired_variant_axioms GeoCoq.Tactics.Coinc.tactics_axioms GeoCoq.Tactics.Coinc.ColR GeoCoq.Meta_theory.Models.POF_to_Tarski GeoCoq.Meta_theory.Counter_models.Planar.independence