quadratic.v

(* Solutions of a quadratic equation over the algebraic numbers *)

Require Import Ssreflect.ssreflect Ssreflect.ssrfun Ssreflect.ssrbool.
Require Import Ssreflect.ssrnat Ssreflect.eqtype Ssreflect.seq.

Require Import MathComp.ssralg MathComp.ssrnum MathComp.algC MathComp.poly.

Section Quadratic.

Local Open Scope ring_scope.

Variables a b c : algC.

Let D := b ^+ 2 - 4%:R * a * c.

Lemma quadratic x : a != 0 ->
                    (a * x ^+ 2 + b * x + c == 0) =
                    (x \in [:: (-b + sqrtC D) / (2%:R * a);
                               (-b - sqrtC D) / (2%:R * a)]).
Proof.
move=> an0.
rewrite (can2_eq (GRing.addrK c) (GRing.subrK c)) GRing.add0r.
rewrite -(inj_eq (GRing.mulfI (_ : 4%:R * a != 0))); last first.
  by rewrite GRing.mulf_eq0 -[0]/(0%:R) eqC_nat.
rewrite GRing.mulrN GRing.mulrDr (GRing.mulrC b).
rewrite -[4 in X in X == _]/((2 * 2)%N) [in X in X == _]GRing.natrM.
rewrite GRing.mulrA -[_ * a * a]GRing.mulrA -(GRing.expr2 a).
rewrite -{1}(GRing.expr2 2%:R) -GRing.exprMn_comm; last exact: GRing.mulrC.
rewrite -GRing.exprMn_comm; last exact: GRing.mulrC.
rewrite -[_ * _ * a]GRing.mulrA -[_ * _ * (x * b)]GRing.mulrA.
rewrite [2%:R * (_ * _)]GRing.mulr_natl GRing.mulrA.
rewrite -(inj_eq (GRing.addIr (b ^+ 2))) -GRing.sqrrD.
rewrite [_ + b ^+ _]GRing.addrC -[b ^+ _ + _]/D -[D in LHS]sqrtCK GRing.eqf_sqr.
rewrite !(can2_eq (GRing.addrK b) (GRing.subrK b)) ![_ - b]GRing.addrC.
have e : 2%:R * a != 0 by rewrite GRing.mulf_eq0 -[0]/(0%:R) eqC_nat.
by rewrite !(can2_eq (GRing.mulKf e) (GRing.mulVKf e)) ![_^-1 * _]GRing.mulrC !inE.
Qed.

End Quadratic.