Qabs_mult@{} : forall a b : Q, abs (a * b) = abs a * abs b. Proof. intros a b. destruct (total_abs_either a) as [Ea|Ea];destruct Ea as [Ea1 Ea2];rewrite Ea2; destruct (total_abs_either b) as [Eb|Eb];destruct Eb as [Eb1 Eb2];rewrite Eb2. - apply ((abs_sig (a*b)).2). apply nonneg_mult_compat;trivial. - rewrite <-negate_mult_distr_r. apply ((abs_sig (a*b)).2). apply nonneg_nonpos_mult;trivial. - rewrite <-negate_mult_distr_l. apply ((abs_sig (a*b)).2). apply nonpos_nonneg_mult;trivial. - rewrite negate_mult_negate. apply ((abs_sig (a*b)).2). apply nonpos_mult;trivial. Qed.
Require Import Import Quoting.Instances. Import NatPair.Instances.