proposition: Lemma two_digits_encoding_inj_lo: forall base a b c d: Z, 0 <= b < base -> 0 <= d < base -> base * a + b = base * c + d -> b = d.
proof: Proof. intros. pose proof Z.mod_unique as P. specialize P with (b := base) (q := c) (r := d). specialize P with (2 := H1). rewrite P by lia. rewrite <- Z.add_mod_idemp_l by lia. rewrite Z.mul_comm. rewrite Z.mod_mul by lia. rewrite Z.add_0_l. rewrite Z.mod_small by lia. reflexivity. Qed.
imports: Coq.Classes.Morphisms Coq.ZArith.BinInt Coq.micromega.Lia Coq.ZArith.ZArith