proposition: Lemma Zunit_eq_one : forall u a : Z, a <> 0%Z -> (a * u)%Z = a -> u = 1%Z.
proof: Proof. intros u a H1 H2. apply unique_unit. intro. apply (Zmult_unit_oneforall u a H1 H2). Qed.
imports: Coq.ZArith.ZArith CoRN.logic.CLogic Coq(Lia)