proposition: Lemma eqmod_uniqueness2 : forall n m l l', l < n -> l' < n -> eqmod n m l' -> eqmod n m l -> l = l'.
proof: Proof. intros n m l l' l_ub l'_ub eqmodnl eqmodnl' ; inversion eqmodnl'. inversion eqmodnl ; intuition lia. rewrite <- H1 in l_ub ; apply False_ind ; clear -l_ub ; intuition lia. Qed.
imports: PeanoNat NArith Lia