proposition: Lemma mag_mult_disj : forall x y, x <> 0 -> y <> 0 -> ((mag (x * y) = (mag x + mag y - 1)%Z :> Z) \/ (mag (x * y) = (mag x + mag y)%Z :> Z)).
proof: Proof. intros x y Zx Zy. destruct (mag_mult beta x y Zx Zy). lia. Qed.
imports: Coq(ZArith Reals Psatz) Core FTZ