proposition: Lemma canonical_Rsqr : forall (a:nonzeroreal) (b c x:R), a * Rsqr x + b * x + c = a * Rsqr (x + b / (2 * a)) + (4 * a * c - Rsqr b) / (4 * a).
proof: Proof. intros. unfold Rsqr. field. apply a. Qed.
imports: Rdefinitions Raxioms RIneq Rbasic_fun