proposition: Lemma Qcabs_mult : forall a b, Qcabs (a*b) = (Qcabs a)*(Qcabs b).
proof: Proof. intros x y. apply (Qcabs_case x); apply (Qcabs_case y); intros Hy Hx. - apply Qcabs_pos. now apply Qcmult_resp_nonneg. - replace (x * (- y)) with (- (x * y)) by ring. apply Qcabs_neg. replace (x * y) with (- (x * (- y))) by ring. replace 0 with (- 0) by ring. apply Qcopp_le_compat. apply Qcopp_le_compat in Hy. now apply Qcmult_resp_nonneg. - replace ((- x) * y) with (- (x * y)) by ring. apply Qcabs_neg. replace (x * y) with (- ((- x) * y)) by ring. replace 0 with (- 0) by ring. apply Qcopp_le_compat. apply Qcopp_le_compat in Hx. now apply Qcmult_resp_nonneg. - apply Qcopp_le_compat in Hx. apply Qcopp_le_compat in Hy. replace (x * y) with (- x * - y) by ring. apply Qcabs_pos. now apply Qcmult_resp_nonneg. Qed.
imports: Qreduction ClassicalRealizability.Qccomplement