proposition: Lemma NatModulo_S_Full : forall n' m, Nat.modulo n' (S m) = m -> Nat.modulo (S n') (S m) = 0.
proof: Proof. autounfold with modulo_db. intros; assert (exists q, divmod (S n') m 0 m = (q, m)). intros; pose proof (divmod_spec n' m 0 m). destruct (divmod n' m 0 m) eqn: ? . destruct H0; eauto. simpl in H. assert (n0 = 0) by (simpl in H; omega). rewrite H2 in *; clear H H2. apply divmod_eq in Heqp. eexists (S n). eapply divmod_eq'; eauto. rewrite Heqp. rewrite <- !minus_n_O, minus_diag, <- plus_n_O. simpl; omega. destruct_ex; simpl in *; rewrite H0; simpl; omega. Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Bedrock.Word Coq.ZArith.ZArith Coq.NArith.NArith Coq.Arith.Arith Coq.Numbers.Natural.Peano.NPeano Coq.Logic.Eqdep_dec Fiat.Narcissus.Common.Specs