proposition: Lemma monotonicity_algebraicMonotonicity : monotonous R -> algebraic_monotonicity.
proof: Proof. unfold monotonous, algebraic_monotonicity; intros. apply H; trivial. Qed.
imports: CoLoR(RelExtras ListExtras TermsEta LogicUtil) Coq(Morphisms)