proposition: Lemma is_linear_ext (l1 l2 : U -> V) : (forall x, l1 x = l2 x) -> is_linear l1 -> is_linear l2.
proof: Proof. intros Hl Hl1. split. intros ; rewrite -!Hl ; apply Hl1. intros ; rewrite -!Hl ; apply Hl1. case: Hl1 => _ _ [M Hl1]. exists M ; split. by apply Hl1. intros ; rewrite -!Hl ; apply Hl1. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Lim_seq Iter Hierarchy Continuity Equiv