proposition: Lemma eqmod_uniqueness : forall n m l l', eqmod n l m -> eqmod n l' m -> l = l'.
proof: Proof. intros n m l l' eqmodnl eqmodnl'. induction eqmodnl. induction eqmodnl'. reflexivity. apply False_ind ; intuition lia. apply IHeqmodnl ; inversion eqmodnl'. apply False_ind ; intuition lia. assert (Temp := proj1 (Nat.add_cancel_l _ _ _) H) ; rewrite <- Temp ; assumption. Qed.
imports: PeanoNat NArith Lia