proposition: Lemma col_213 a b c : Col (Point R) (@bet' R) a b c -> Col (Point R) (@bet' R) b a c.
proof: Proof. by rewrite /Col bet'_sym [bet' b c a]bet'_sym [bet' c a b]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.Meta_theory.Models.POF_to_Tarski GeoCoq.Meta_theory.Counter_models.Planar.independence