proposition: Lemma two_digits_encoding_inj_hi: forall base a b c d: Z, 0 <= b < base -> 0 <= d < base -> base * a + b = base * c + d -> a = c.
proof: Proof. intros. nia. Qed.
imports: Coq.Classes.Morphisms Coq.ZArith.BinInt Coq.micromega.Lia Coq.ZArith.ZArith