proposition: Theorem spec_mul_normc_bis : forall x y : Qc, [mul_norm (of_Qc x) (of_Qc y)] = x*y.
proof: Proof. intros. rewrite <- strong_spec_mul_norm by apply strong_spec_of_Qc_bis. rewrite strong_spec_red. symmetry; apply (Qred_complete (x*y)%Q). rewrite spec_mul_norm, ! strong_spec_of_Qc; auto with qarith. Qed.
imports: BigNumPrelude Lia QArith Qcanon Qpower Qminmax NSig ZSig QSig