proposition: Lemma smaller : forall x y : R, [0] [<] x -> [0] [<] y -> {z : R | [0] [<] z | z [<=] x /\ z [<=] y}.
proof: Proof. intros x y H H0. elim (less_cotransitive_unfolded _ _ _ (half_3 _ _ H) y); intro. exists (Half[*]x). apply mult_resp_pos. apply pos_half. auto. split; apply less_leEq. apply half_3. auto. auto. cut (Half[*]y [<] y). intro. exists (Half[*]y). apply mult_resp_pos. apply pos_half. auto. split; apply less_leEq. apply less_transitive_unfolded with y. auto. auto. auto. apply half_3. auto. Qed.
imports: CoRN.algebra.COrdAbs Coq(Lia)