proposition: Lemma norm_factor_gt_0 : 0 < norm_factor.
proof: Proof. rewrite <- (Rmult_1_r norm_factor). rewrite <- norm_zero. rewrite -(plus_opp_r zero). apply (norm_compat2 _ _ (mkposreal _ Rlt_0_1)). apply ball_center. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Markov Iter Lub