proposition: Theorem spec_mod_gt: forall x y, [x] > [y] -> 0 < [y] -> [mod_gt x y] = [x] mod [y].
proof: Proof. intros x y. rewrite mod_gt_fold. apply spec_iter; clear x y. intros n x y H1 H2. simpl. rewrite spec_reduce. exact (ZnZ.spec_modulo_gt x y H1 H2). intros n m x y H1 H2. cbv zeta beta. rewrite spec_reduce. rewrite <- spec_mk_t in H1. rewrite <- (spec_get_endn n (S m) y x); auto with zarith. rewrite spec_mk_t. apply ZnZ.spec_modulo_gt; auto. rewrite <- (spec_get_endn n (S m) y x), !spec_mk_t in H1; auto with zarith. rewrite <- (spec_get_endn n (S m) y x), !spec_mk_t in H2; auto with zarith. intros n m x y H1 H2. unfold wn_modn1. rewrite spec_reduce. unfold eval; rewrite nmake_double. apply (spec_modn1 n); auto. intros n m x y H1 H2; unfold mod_gtnm. repeat rewrite spec_reduce_n. rewrite (spec_cast_l n m x), (spec_cast_r n m y). unfold to_Z; apply ZnZ.spec_modulo_gt. rewrite (spec_cast_l n m x) in H1; auto. rewrite (spec_cast_r n m y) in H1; auto. rewrite (spec_cast_r n m y) in H2; auto. Qed.
imports: Bool BigNumPrelude ZArith Lia Nnat Ndigits CyclicAxioms DoubleType Nbasic Wf_nat StreamMemo NSig NMake_gen