proposition: Theorem spec_sub0 : forall x y, [x] < [y] -> [sub x y] = 0.
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. unfold interp_carry in H. generalize (ZnZ.spec_to_Z z); auto with zarith. exact spec_0. Qed.
imports: Bool BigNumPrelude ZArith Lia Nnat Ndigits CyclicAxioms DoubleType Nbasic Wf_nat StreamMemo NSig NMake_gen