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