proposition: Lemma surjectif : forall n m p, m < n -> eqmod n m (n * p + m).
proof: Proof. intros n m p m_ub ; induction p. replace (n * 0) with 0 by lia ; constructor ; assumption. replace ((n * S p) + m) with (n + ((n * p) + m)). constructor ; assumption. rewrite Nat.mul_succ_r ; lia. Qed.
imports: PeanoNat NArith Lia