proposition: Lemma col_trans x y a b c : x <> y -> col' x y a -> col' x y b -> col' x y c -> col' a b c.
proof: Proof. rewrite /col'; set c0 := x 0 0 - y 0 0; set c1 := x 0 1 - y 0 1. move=> /eqP xy_neq; rewrite eq_sym -subr_eq0 -mulNr=> /eqP E1. rewrite eq_sym -subr_eq0 -mulNr=> /eqP E2. rewrite eq_sym -subr_eq0 -mulNr=> /eqP E3. move: (upper_dim_aux E2 E1) (upper_dim_aux E3 E2). move/eqP: E1; move/eqP: E2; move/eqP: E3=> E3 E2 E1. set ba0 := a 0 0 - b 0 0; set ba1 := a 0 1 - b 0 1; set cb0 := b 0 0 - c 0 0; set cb1 := b 0 1 - c 0 1; move=> E4 E5. have: (c0 * c1 * (ba0 * cb1) == c0 * c1 * (ba1 * cb0)). rewrite mulrCA [c0*c1]mulrC -mulrA mulrCA mulrA E4 eq_sym. rewrite [X in X == _]mulrCA [c1*c0]mulrC -mulrA E5 mulrCA mulrA. by rewrite mulNr mulrN -mulNr -mulNr [X in _ * X]mulNr mulrN -mulNr -mulNr. rewrite -subr_eq0 -mulrBr mulf_eq0 subr_eq0=> /orP[|//]; rewrite mulf_eq0. move: xy_neq; rewrite -subr_eq0 vector2_eq !mxE=> NE1 NE2; move: E1 E2 E3; move: NE2 NE1; rewrite /c0 /c1; move=> /orP[/eqP ->|/eqP ->]; rewrite eqxx /= ?orbF !mulNr !mul0r ?subr0 ?sub0r ?oppr_eq0 !mulf_eq0. case: (x 0 1 - y 0 1 =P 0)=> //= _ _; rewrite !subr_eq0 /ba0 /cb1 /ba1 /cb0. by move=> /eqP -> /eqP -> /eqP ->; rewrite subrr mulr0 mul0r eqxx. case: (x 0 0 - y 0 0 =P 0)=> //= _ _; rewrite !subr_eq0 /ba0 /cb1 /ba1 /cb0. by move=> /eqP -> /eqP -> /eqP ->; rewrite subrr mulr0 mul0r eqxx. 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