proposition: Lemma AbsSmall_pos_reflexive : forall x : OF, ([0][<=]x) -> AbsSmall x x.
proof: Proof. intros. split. apply leEq_transitive with (y := [0]:OF). apply inv_cancel_leEq. rstepl ([0]:OF). rstepr x. assumption. assumption. apply leEq_reflexive. Qed.
imports: CoRN.reals.Q_in_CReals