proposition: Lemma eqmod_uniqueness1 : forall n m l, l < n -> eqmod n l m -> forall p, p < n -> p <> l -> ~eqmod n p m.
proof: Proof. intros n m l l_ub eqmodnl p p_ub p_neq Hf ; induction eqmodnl. inversion Hf ; intuition lia. apply IHeqmodnl. assumption. assumption. inversion Hf. assert (Temp := eqmod_bounded _ _ _ Hf). apply False_ind ; clear -H1 Temp ; intuition lia. assert (Temp := proj1 (Nat.add_cancel_l _ _ _) H) ; rewrite <- Temp ; assumption. Qed.
imports: PeanoNat NArith Lia