proposition: Lemma is_linear_id : is_linear (fun (x : V) => x).
proof: Proof. repeat split. - exists 1 ; split. exact Rlt_0_1. move => x ; rewrite Rmult_1_l. by apply Rle_refl. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Lim_seq Iter Hierarchy Continuity Equiv