proposition: Corollary divmod_eq'' : forall x y, x = (y - (snd (divmod x y 0 y))) + (fst (divmod x y 0 y)) * (S y).
proof: Proof. intros; rewrite plus_comm; destruct (divmod x y 0 y) eqn: ? . simpl; eapply divmod_eq; assumption. Defined.
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