proposition: Lemma AbsSmall_sqr : forall x e : IR, AbsSmall e x -> x[^]2 [<=] e[^]2.
proof: Proof. unfold AbsSmall in |- *. intros. elim H. clear H. intros. astepl ([0][+]x[^]2). apply shift_plus_leEq. astepr ((e[-]x) [*] (e[+]x)). apply mult_resp_nonneg. apply shift_leEq_minus. astepl x. auto. rstepr (x[-][--]e). apply shift_leEq_minus. astepl ( [--]e). auto. Qed.
imports: CoRN.complex.AbsCC Coq(Lia)