proposition: Lemma bet'_sym a b c : bet' a b c = bet' c b a.
proof: Proof. by rewrite /bet' bet_sym [bet (a 0 1)%:M (b 0 1)%:M (c 0 1)%:M] bet_sym. 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.Meta_theory.Models.POF_to_Tarski GeoCoq.Meta_theory.Counter_models.Planar.independence