proposition: Lemma Tle_inject_mono : opT.Trel_monotone Tle_inject.
proof: Proof. unfold Tle_inject; intros f l1 l2 H; simpl; apply Tle_mono; induction H; [ left | right ]; assumption. Qed.
imports: Coq(Setoid List Relations Wellfounded PeanoNat) CoLoR(weaved_relation list_permut terminaison)