proposition: Lemma Rmax_eq_l : forall r1 r2, r2 <= r1 -> Rmax r1 r2 = r1.
proof: Proof. intros r1 r2 r1_le_r2 ; unfold Rmax ; destruct (Rle_dec r1 r2). destruct r. apply False_ind ; apply Rlt_irrefl with r2 ; apply Rle_lt_trans with r1 ; assumption. symmetry ; trivial. reflexivity. Qed.
imports: RIneq MyNeq Rfunctions Lra