proposition: Lemma col_perm_2 a b c : col' a b c = col' a c b.
proof: Proof. apply /eqP/eqP=> /eqP H; move: (col_2D H)=> H'; apply /eqP; apply col_2D'. elim H'; clear H'; [|move=> H'; elim H'; clear H']; rewrite bet_sym; tauto. elim H'; clear H'; [|move=> H'; elim H'; clear H']; rewrite bet_sym; tauto. 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