proposition: Lemma sMax_plus_cte_right : forall k (f:nat->U), sMax (fun n => f n + k) == UPlus <_> k @ sMax f.
proof: Proof. intros; apply fmon_eq_intro; simpl; intros. induction n; simpl; intros; auto. rewrite IHn; auto. Qed.
imports: ALEA(Utheory)