proposition: Lemma Rmin_ge_0 : forall x y, 0 <= x -> 0 <= y -> 0 <= Rmin x y.
proof: Proof. intros x y x_pos y_pos. unfold Rmin ; case (Rle_dec x y) ; intro h ; intuition. Qed.
imports: Rsequence_def Rpser_def Rpow_facts Cmet Cnorm Ctacfield Cpow Cprop_base Csequence_def Csequence_facts Cpser_def Lia