proposition: Lemma divmod_eq' : forall x y q u, (u <= y)%nat -> x = q * (S y) + (y - u) -> divmod x y 0 y = (q, u).
proof: Proof. intros; pose proof (divmod_spec x y 0 y). destruct (divmod x y 0 y); destruct H1; eauto. rewrite H0 in H1. simpl in H1. rewrite minus_diag, <- mult_n_O, <- !plus_n_O in *. assert (n + y * n = n * S y) by (rewrite mult_succ_r, plus_comm, mult_comm; reflexivity). f_equal; eapply (@minus_inj' n q y n0 u); eauto; rewrite !mult_succ_r in *; rewrite !Nat.add_sub_assoc in H1; eauto; 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