proposition: Lemma disjoints : forall n, 0 < n -> forall m, {k | k < n /\ eqmod n k m /\ forall l, l <> k -> ~ eqmod n l m}.
proof: Proof. intros n n_pos m ; apply disjoints_prelim with (M:= (S m)) ; intuition (auto with arith). Qed.
imports: PeanoNat NArith Lia