proposition: Lemma mag_d: (0< F2R d)%R -> (mag beta (F2R d) = mag beta x :>Z).
proof: Proof. Proof with auto with typeclass_instances. intros Y. rewrite d_eq; apply mag_DN... now rewrite <- d_eq. Qed.
imports: Coq(ZArith Reals Psatz) Core Operations