proposition: Lemma Tlt_monotone_afs : Trel_monotone Tlt_afs.
proof: Proof. apply gen_monotone_afs; [ apply Tlt_trans | apply Tlt_mono ]. Qed.
imports: Coq(Setoid List Relations Wellfounded PeanoNat) CoLoR(weaved_relation list_permut terminaison)