proposition: Lemma bet_in_disk (a b c : Vector) : (a *m a^T) 0 0 < 1 -> (c *m c^T) 0 0 < 1 -> bet a b c -> (b *m b^T) 0 0 < 1.
proof: Proof. move=> a_in_disk c_in_disk. rewrite /bet => /orP[/betEP [ [H _] | H | H ] |H ] ; rewrite -?H ?a_in_disk ?H ?c_in_disk //. move: H. rewrite betS_neq13=> /andP [/betSP [H1 H2 H3] H4]. have: (c *m a^T) 0 0 < 1 by rewrite dotC p_scalar_lt1 //. move=> ca_lt1. move/eqP: H1;rewrite subr_eq => /eqP ->. set r := betR a b c. rewrite -[X in _ + X]scale1r scalerBr addrAC -addrA -scalerBl. rewrite mulmxDl -!scalemxAl dotC [X in _ + (_ *: X)]dotC. rewrite !mulmxDl -!scalemxAl [a *m c^T]dotC !scalerDr !scalerA. rewrite addrA. apply lt_le_trans with (r * r * 1 + r * (1 - r) * 1 + (1 - r) * r * 1 + (1 - r) * (1 - r) * 1). rewrite !mxE ?ltr_add //; rewrite -subr_gt0 -mulrBr ?pmulr_rgt0 ?subr_gt0 //. move: c_in_disk ; rewrite !mxE //. move: ca_lt1 ; rewrite !mxE //. move: ca_lt1 ; rewrite !mxE //. move: a_in_disk ; rewrite !mxE //. rewrite !mulr1 !mulrBl !mulrBr !mul1r !mulr1. rewrite [r * r + (r -r * r)]addrCA subrr addr0. rewrite [(1 - r) - (r - r * r)]addrC addrA addrC. rewrite -[r + (r - r * r) - (r - r * r)]addrA subrr addr0. by rewrite addrAC -addrA subrr addr0 lexx. 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