proposition: Lemma E_in_disk_aux b c d (E': Vector) : cong_v (#b) E' (#c) (#d) -> (E' *m (E')^T) 0 0 < 1.
proof: Proof. move=> cong_v_bE'cd. rewrite -subr_gt0. move:cong_v_bE'cd. rewrite /cong_v -!/(omd _ _) eq_sym. have: 0 < omd c d ^+ 2 / (omd c c * omd d d) by rewrite mulr_gt0 ?invr_gt0 ?expr2 ?mulr_gt0 ?omd_gt0. move => H1 /eqP H2. move: H1 ; rewrite H2 lt0r. rewrite lt0r invfM mulrA. move => /andP[neq0 ge0]. apply /andP. split. move: neq0. by rewrite mulf_eq0 negb_or invr_eq0 => /andP[_ ->]. move: ge0. rewrite pmulr_rge0 ?invr_ge0 //. rewrite lt0r mulr_ge0 ?invr_ge0 ?omd_ge0 ?sqr_ge0 // andbT. move: neq0. by rewrite mulf_eq0 negb_or=> /andP[-> _]. 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 algC) mathcomp(zmodp) GeoCoq.Meta_theory.Models.POF_to_Tarski GeoCoq.Axioms.gupta_inspired_variant_axioms GeoCoq.Meta_theory.Models.tarski_to_gupta_inspired GeoCoq.Tarski_dev.Ch06_out_lines GeoCoq.Tarski_dev.Ch11_angles GeoCoq.Meta_theory.Parallel_postulates.parallel_postulates GeoCoq.Meta_theory.Counter_models.Planar.independence