proposition: Lemma Rmax_abs : forall a b : R, Rmax (Rabs a) (Rabs b) >= 0.
proof: Proof. intros. apply (Rge_trans _ (Rabs a) _). apply Rle_ge. apply Rmax_l. apply (Rle_ge 0 (Rabs a)). apply Rabs_pos. Qed.
imports: Lra Coq.Reals.Reals Reals.ROrderedType Notations