proposition: Lemma min_spec_1 : forall n m : Rdefinitions.R, (Rdefinitions.Rle m n /\ Rbasic_fun.Rmin m m = m) \/ (Rdefinitions.Rlt n m /\ Rbasic_fun.Rmin m n = n).
proof: Proof. hammer. Restart. hauto use: RIneq.Rnot_le_lt unfold: Rbasic_fun.Rmin. Qed.
imports: Hammer(Hammer) Arith List