proposition: Lemma ratio_inv v1 v2 : v1 != 0 -> v2 != 0 -> v1 == ratio v1 v2 *: v2 -> ratio v1 v2 = 1 / ratio v2 v1.
proof: Proof. move=> NE1 NE2 /eqP E; apply /eqP; rewrite eq_sym /ratio {2}E /ratio. case: pickP=> [x /eqP px|/all_v_neq0 //]; case: pickP=> [y py|/all_v_neq0 //]. rewrite mxE [X in _ / (_ / X)]mulrC -{1}[v2 0 x]mulr1 -mulf_div mulfV ?mul1r; rewrite ?invf_div //; by apply /eqP=> px'; apply px; rewrite E mxE px' mulr0. 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