proposition: Theorem Rmin_compare : forall x y, Rmin x y = match Rcompare x y with Lt => x | Eq => x | Gt => y end.
proof: Proof. intros x y. unfold Rmin. destruct (Rle_dec x y) as [[Hx|Hx]|Hx]. now rewrite Rcompare_Lt. now rewrite Rcompare_Eq. rewrite Rcompare_Gt. easy. now apply Rnot_le_lt. Qed.
imports: Coq(Psatz Reals ZArith) Zaux