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