proposition: Lemma mag_sqrt_disj : forall x, 0 < x -> (mag x = 2 * mag (sqrt x) - 1 :> Z)%Z \/ (mag x = 2 * mag (sqrt x) :> Z)%Z.
proof: Proof. intros x Px. rewrite (mag_sqrt beta x Px). generalize (Zdiv2_odd_eqn (mag x + 1)). destruct Z.odd ; intros ; lia. Qed.
imports: Coq(ZArith Reals Psatz) Core FTZ