proposition: Lemma sqrt_mult_opp : forall a b, 0 >= a -> 0 >= b -> sqrt (a * b) = sqrt (-a) * sqrt (-b).
proof: Proof. intros a b H H1. rewrite <- (sqrt_mult (-a) (-b)). intuition (auto with real). intuition (auto with real). intuition (auto with real). Qed.
imports: ZArith Reals Lia Lra DiscrR Rfunctions