proposition: Lemma par_strictP a b c d : par_strict a b c d <-> Par_strict (@Point R) (@bet' R) a b c d.
proof: Proof. split; [move=> [? HF]|move => [? [? [? HF]]]]; last first. - repeat (split=> //); try (by apply coplanarP). by move=> [x [? ?]]; apply HF; exists x; split; apply colP. repeat (split=> //); try (by apply coplanarP); last by move=> [x [? ?]]; apply HF; exists x; split; apply colP. - move => abP; apply HF; exists c; rewrite abP; split; apply colP; [left|right; right]; by rewrite /bet' bet_axx eqxx andTb implybT. - move => cdP; apply HF; exists a; rewrite cdP; split; apply colP; [right; right|left]; by rewrite /bet' bet_axx eqxx andTb implybT. 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