proposition: Lemma roots_poly2 (a b c: R) (d := b^+2 - 4%:R * a * c): a != 0 -> d >= 0 -> let r1 := (- b - Num.sqrt d) / 2%:R / a in let r2 := (- b + Num.sqrt d) / 2%:R / a in a * r1^+2 + b * r1 + c == 0 /\ a * r2^+2 + b * r2 + c == 0.
proof: Proof. move=> a_neq0 d_ge0 r1 r2. have: 4%:R * a * c * (2%:R^-1 / a) ^+ 2 == c / a. rewrite exprMn !exprVn mulrCA !mulrA [2%:R ^- 2 * 4%:R]mulrC. rewrite /GRing.natmul /= expr2 mulrDl mul1r !addrA. rewrite divff ?lt0r_neq0 ?addr_gt0 ?ltr01 //. rewrite mul1r expr2 mulrAC invfM mulrA divff //. by rewrite mul1r mulrC. move => /eqP H1. have: (2%:R^-1 + 2%:R^-1) == 1 :> R. by rewrite /GRing.natmul /= -[(1 + 1)^-1]mul1r -mulrDl divff ?lt0r_neq0 ?addr_gt0 ?ltr01. move=> /eqP H2. have: a * ((r1+b/2%:R/a)^+2-d* (2%:R^-1 / a) ^+ 2 ) == 0. rewrite /r1 -!mulrDl [(- b - Num.sqrt d + b)]addrC addrA subrr. by rewrite add0r -mulrA exprMn sqrrN sqr_sqrtr ?subrr ?mulr0. rewrite sqrrD /d mulrBl H1 -exprMn mulrA mulrA mulrA opprD opprK !addrA. rewrite mulrDr [a * (c / a)]mulrCA divff // mulr1. rewrite -!addrA subrr addr0 -mulrDl -mulrDr H2 mulr1. rewrite mulrDr [a * (r1 * b / a)]mulrCA divff // mulr1. rewrite !addrA [r1*b]mulrC => ->. have: a * ((r2+b/2%:R/a)^+2-d* (2%:R^-1 / a) ^+ 2 ) == 0. rewrite /r2 -!mulrDl [(- b + Num.sqrt d + b)]addrC addrA subrr. by rewrite add0r -mulrA exprMn sqr_sqrtr ?subrr ?mulr0. rewrite sqrrD /d mulrBl H1 -exprMn mulrA mulrA mulrA opprD opprK !addrA. rewrite mulrDr [a * (c / a)]mulrCA divff // mulr1. rewrite -!addrA subrr addr0 -mulrDl -mulrDr H2 mulr1. rewrite mulrDr [a * (r2 * b / a)]mulrCA divff // mulr1. by rewrite !addrA [r2*b]mulrC => ->. 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