proposition: Theorem spec_sub_norm : forall x y, [sub_norm x y] == [x] - [y].
proof: Proof. intros x y; unfold sub_norm; rewrite spec_add_norm; auto. rewrite spec_opp; ring. Qed.
imports: BigNumPrelude Lia QArith Qcanon Qpower Qminmax NSig ZSig QSig