proposition: Theorem spec_add : forall x y, [add x y] == [x] + [y].
proof: Proof. intros [x | nx dx] [y | ny dy]; unfold Qplus; qsimpl. 1-2, 4, 6: lia. rewrite Pos.mul_1_r, Z2Pos.id; auto. rewrite Pos.mul_1_r, Z2Pos.id; auto. rewrite Pos2Z.inj_mul, 2 Z2Pos.id; auto. Qed.
imports: BigNumPrelude Lia QArith Qcanon Qpower Qminmax NSig ZSig QSig