proposition: Lemma strictly_preserving_preserves_pos : (forall x, 0 < x -> 0 < f x) -> StrictlyOrderPreserving f.
proof: Proof. intros E. repeat (split; try apply _). intros x y F. destruct (decompose_lt F) as [z [Ez1 Ez2]]. apply compose_lt with (f z). - apply E. trivial. - rewrite Ez2, (preserves_plus (f:=f)). trivial. Qed.
imports: HoTT.Classes.theory.apartness HoTT.Classes.interfaces.abstract_algebra HoTT.Classes.interfaces.orders HoTT.Classes.theory.rings HoTT.Classes.orders.orders HoTT.Classes.orders.maps