proposition: Lemma mag_minus_disj : forall x y, 0 < x -> 0 < y -> (mag y <= mag x - 2)%Z -> ((mag (x - y) = mag x :> Z) \/ (mag (x - y) = (mag x - 1)%Z :> Z)).
proof: Proof. intros x y Px Py Hln. assert (Hxy : y < x); [now apply (lt_mag beta); [ |lia]|]. generalize (mag_minus beta x y Py Hxy); intro Hln2. generalize (mag_minus_lb beta x y Px Py Hln); intro Hln3. lia. Qed.
imports: Coq(ZArith Reals Psatz) Core FTZ