proposition: Lemma restrict_mono: Proper (le ++> eq ==> le) restrict.
proof: Proof. intros x y lexy S ? <-. split. - intros z [inz ltz]; split; trivial. eapply lt_le_trans; eauto. - intros x' y' [inx' ltx'] [iny' lty'] ltx'y'. split; trivial. clear ltx'. eapply le_lt_trans; eauto. Qed.
imports: Coq(Relations Equivalence Morphisms Utf8) Coq(ChoiceFacts ClassicalFacts) Coq.Program(Basics) Coq.Logic(SetoidChoice)