proposition: Lemma ratio_1D (v1 v2 : 'rV[R]_(1)) : v2 != 0 -> v1 == ratio v1 v2 *: v2.
proof: Proof. rewrite /ratio; case: pickP=> [x|/all_v_neq0 //]; case: x=> ? ?. rewrite ord1=> ? ?; apply /eqP /matrixP=> i j; case: i; case: j=> ? ? ? ?. by rewrite !ord1 !mxE mulrAC -mulrA divff // mulr1. 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