proposition: Lemma pos_half : ([0]:R) [<] Half.
proof: Proof. apply mult_cancel_pos_lft with (Two:R). apply (pos_wd R (Half[*]Two) [1]). exact half_1. apply pos_one. apply less_leEq; apply pos_two. Qed.
imports: CoRN.algebra.COrdFields Coq(Lia)