proposition: Lemma col_2D' a b c : (bet a b c \/ bet b c a \/ bet c a b) -> (a 0 0 - b 0 0) * (b 0 1 - c 0 1) == (a 0 1 - b 0 1) * (b 0 0 - c 0 0).
proof: Proof. rewrite /bet /betE. case: (a =P b)=> [->|]; first by rewrite !subrr !mul0r eqxx. move=> ab_neq; case: (b =P c)=> [->|]; first by rewrite !subrr !mulr0 eqxx. move=> bc_neq; case: (c =P a)=> [->|ca_neq] /=; [|move=> HC]. by rewrite -[b 0 1 - a 0 1]opprB mulrN -mulNr opprB mulrC. elim HC; clear HC; [|move=> HC; elim HC; clear HC]; move=> /betSP'[E0 E1 _ _]. rewrite -[b 0 0 - c 0 0](addrBDB _ (a 0 0)) -[a 0 0 - b 0 0]opprB E0. rewrite -[b 0 1 - c 0 1](addrBDB _ (a 0 1)) -[a 0 1 - b 0 1]opprB E1. rewrite -[a 0 0 - c 0 0]opprB -{3}[c 0 0 - a 0 0]mul1r. rewrite -[a 0 1 - c 0 1]opprB -{2}[c 0 1 - a 0 1]mul1r. rewrite -!mulrBl mulrCA [X in _ == X]mulrCA !mulNr -!mulrA. by rewrite [X in _ * - (_ * X)]mulrC. rewrite -[b 0 0 - c 0 0]opprB E0 -[b 0 1 - c 0 1]opprB E1 !mulrN mulrCA. by rewrite [X in _ * X]mulrC eq_sym mulrCA. rewrite -[a 0 0 - b 0 0](addrBDB _ (c 0 0)) -[a 0 1 - b 0 1](addrBDB _ (c 0 1)). rewrite E0 E1 -[c 0 0 - b 0 0]opprB -[c 0 1 - b 0 1]opprB -[X in _ - X]mul1r. by rewrite eq_sym -[X in _ - X]mul1r -!mulrBl mulrAC. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun ssrnat eqtype seq order) mathcomp(fintype bigop) mathcomp(ssralg ssrnum matrix) mathcomp(zmodp) GeoCoq.Axioms.tarski_axioms GeoCoq.Axioms.gupta_inspired_variant_axioms GeoCoq.Meta_theory.Models.gupta_inspired_to_tarski GeoCoq.Meta_theory.Counter_models.coplanarity GeoCoq.Meta_theory.Parallel_postulates.parallel_postulates GeoCoq.Tarski_dev.Ch12_parallel_inter_dec