proposition: Lemma mag_div_disj : forall x y : R, 0 < x -> 0 < y -> ((mag (x / y) = mag x - mag y :> Z)%Z \/ (mag (x / y) = mag x - mag y + 1 :> Z)%Z).
proof: Proof. intros x y Px Py. generalize (mag_div beta x y (Rgt_not_eq _ _ Px) (Rgt_not_eq _ _ Py)). lia. Qed.
imports: Coq(ZArith Reals Psatz) Core FTZ