proposition: Lemma norm_zero : norm zero = 0.
proof: Proof. apply Rle_antisym. - rewrite -(scal_zero_l zero). rewrite -(Rmult_0_l (norm zero)). rewrite -(@abs_zero K). apply norm_scal. - apply Rplus_le_reg_r with (norm zero). rewrite Rplus_0_l. rewrite -{1}[zero]plus_zero_r. exact (norm_triangle zero zero). Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Markov Iter Lub