proposition: Lemma Qabs_mult@{} : forall a b : Q, abs (a * b) = abs a * abs b.
proof: 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.
imports: HoTT.Classes.implementations.peano_naturals HoTT.Classes.implementations.natpair_integers HoTT.Classes.interfaces.abstract_algebra HoTT.Classes.interfaces.naturals HoTT.Classes.interfaces.rationals HoTT.Classes.interfaces.orders HoTT.Classes.theory.groups HoTT.Classes.theory.integers HoTT.Classes.theory.dec_fields HoTT.Classes.orders.sum HoTT.Classes.orders.dec_fields HoTT.Classes.orders.lattices HoTT.Classes.theory.additional_operations HoTT.Classes.tactics.ring_quote HoTT.Classes.tactics.ring_tac