proposition: Lemma bet_symmetry : ~ bet_symmetryP Point bet'.
proof: Proof. move => HF; move: (HF (@c2D R) (@a2D R) (@a2D R)). rewrite /bet' bet_xxa bet_axx !mxE /= !eqxx (eq_sym (@a2D R)) ca_neq_2D /=. by apply /implyP. 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