proposition: Lemma minus_inj : forall m m' y q q', (q < y)%nat -> (q' < y)%nat -> (m * y) + y - q = (m' * y) + y - q' -> m = m' /\ q = q'.
proof: Proof. induction m; simpl; intros. - destruct m'. + simpl in *; intuition. + rewrite mult_succ_l in *. assert (y - q < (m' * y) + y + y - q')%nat. { clear H1; induction (m' * y); intros. - omega. - etransitivity. apply IHn. omega. } exfalso. rewrite H1 in H2. omega. - destruct m'. + simpl in *. assert (y - q' < (m * y) + y + y - q)%nat. { clear H1 IHm; induction (m * y); intros. - omega. - etransitivity. apply IHn. omega. } exfalso. rewrite <- H1 in H2; omega. + destruct (IHm m' _ _ _ H H0). simpl in H1. rewrite <- !Nat.add_sub_assoc in H1; try omega. subst; intuition. 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