proposition: Lemma Zmult_unit_oneforall : forall u a : Z, a <> 0%Z -> (a * u)%Z = a -> forall b : Z, (b * u)%Z = b.
proof: Proof. intros u a H0 Hu b. apply (Zmult_absorb a). assumption. rewrite Zmult_assoc. rewrite (Zmult_comm a b). rewrite <- Zmult_assoc. rewrite Hu. reflexivity. Qed.
imports: Coq.ZArith.ZArith CoRN.logic.CLogic Coq(Lia)