proposition: Theorem spec_div_normc_bis : forall x y : Qc, [div_norm (of_Qc x) (of_Qc y)] = x/y.
proof: Proof. intros. rewrite <- strong_spec_div_norm by apply strong_spec_of_Qc_bis. rewrite strong_spec_red. symmetry; apply (Qred_complete (x*(/y)%Qc)%Q). rewrite spec_div_norm, ! strong_spec_of_Qc. unfold Qcinv, Q2Qc, this; rewrite Qred_correct; auto with qarith. Qed.
imports: BigNumPrelude Lia QArith Qcanon Qpower Qminmax NSig ZSig QSig