proposition: Theorem spec_sub_pos : forall x y, [y] <= [x] -> [sub x y] = [x] - [y].
proof: Proof. intros x y. rewrite sub_fold. apply spec_same_level. clear x y. intros n x y. simpl. generalize (ZnZ.spec_sub_c x y); destruct ZnZ.sub_c as [z|z]; intros H LE. rewrite spec_reduce. assumption. unfold interp_carry in H. exfalso. generalize (ZnZ.spec_to_Z z); auto with zarith. Qed.
imports: Bool BigNumPrelude ZArith Lia Nnat Ndigits CyclicAxioms DoubleType Nbasic Wf_nat StreamMemo NSig NMake_gen