proposition: Lemma divmod_eq : forall x y q u, divmod x y 0 y = (q, u) -> x = q * (S y) + (y - u).
proof: Proof. intros; pose proof (divmod_spec x y 0 y). rewrite H in H0; destruct H0; eauto. simpl in H0. assert (x = q + y * q + (y - u)) by omega. rewrite H2. rewrite mult_succ_r. rewrite (plus_comm (q * y) q). rewrite mult_comm; f_equal. 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