proposition: Lemma inl_restr_prop S J (H:sub_right_directed J(isr S)) : inductive_system_on (inl_restr H) (restr (isE S) J) J (induced_order (isr S) J) (restr (isf S) (induced_order (isr S) J)).
proof: Proof. by []. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)