proposition: Theorem spec_add_norm : forall x y, [add_norm x y] == [x] + [y].
proof: Proof. intros x y; rewrite <- spec_add. destruct x; destruct y; unfold add_norm, add; destr_eqb; auto using Qeq_refl, spec_norm. Qed.
imports: BigNumPrelude Lia QArith Qcanon Qpower Qminmax NSig ZSig QSig