proposition: Theorem spec_sub_normc_bis : forall x y : Qc, [sub_norm (of_Qc x) (of_Qc y)] = x-y.
proof: Proof. intros. rewrite <- strong_spec_sub_norm by apply strong_spec_of_Qc_bis. rewrite strong_spec_red. symmetry; apply (Qred_complete (x+(-y)%Qc)%Q). rewrite spec_sub_norm, ! strong_spec_of_Qc. unfold Qcopp, Q2Qc, this. rewrite Qred_correct ; auto with qarith. Qed.
imports: BigNumPrelude Lia QArith Qcanon Qpower Qminmax NSig ZSig QSig