proposition: Lemma Tle_monotone_afs : Trel_monotone Tle_afs.
proof: Proof. apply gen_monotone_afs; [ apply Tle_trans | apply Tle_mono ]. Qed.
imports: Coq(Setoid List Relations Wellfounded PeanoNat) CoLoR(weaved_relation list_permut terminaison)