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