proposition: Lemma upper_dim_aux (a b m : 'rV[R]_2) (c0 c1: R) : c0 * (m 0 0 - a 0 0) + c1 * (m 0 1 - a 0 1) = 0 -> c0 * (m 0 0 - b 0 0) + c1 * (m 0 1 - b 0 1) = 0 -> c0 * (b 0 0 - a 0 0) = - c1 * (b 0 1 - a 0 1).
proof: Proof. move=> /eqP E1 /eqP E2; move: E1 E2; rewrite !addr_eq0 -!mulNr. move=> /eqP E1 /eqP E2; apply /eqP; rewrite -(addrBBB (m 0 0)) eq_sym. by rewrite -(addrBBB (m 0 1)) mulrBr eq_sym mulrBr -E1 -E2. 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