proposition: Lemma ratio_e0_n1 (v1 v2 : 'rV[R]_2) : v2 0 0 = 0 -> v2 0 1 != 0 -> ratio v1 v2 = v1 0 1 / v2 0 1.
proof: Proof. move=> E NE; rewrite /ratio; case: pickP=> [x|/all_v_neq0 H]; [elim x=> m i|]; last by move: H; rewrite vector2_neq0 NE orbT=> H; exfalso; apply H. have: ((m == 1)%N || (m == 0)%N) by rewrite -leqn0 -ltnS -leq_eqVlt -ltnS. move=> /orP[/eqP E'|/eqP E']; move: i; rewrite E'=> i. by rewrite (@ord_inj _ (Ordinal i) 1) // (@ord_inj _ (Ordinal p) 0). by rewrite (@ord_inj _ (Ordinal i) 0) // E=> /eqP NE'. 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