proposition: Lemma is_linear_opp : is_linear (@opp V).
proof: Proof. repeat split. - move => x y. apply (opp_plus x y). - move => k x. apply sym_eq. apply: scal_opp_r. - exists 1 ; split. exact Rlt_0_1. move => x ; rewrite norm_opp Rmult_1_l. by apply Rle_refl. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Lim_seq Iter Hierarchy Continuity Equiv