proposition: Lemma Exercise2_7h u v: inductive r -> worder r -> inc u (closures) -> inc v (closures) -> has_supremum (closure_ordering) (doubleton u v).
proof: Proof. move=> ir [_ wor] uc vc; apply: Exercise2_7g => //. move=> x xsr. set y := (Ixf x (compose u v)). have sy: sub y (substrate r) by apply: Zo_S. move: (inductive_max_greater or ir xsr) => [m [ms mm xm]]. move: uc vc => /Zo_P [p1 p2] => /Zo_P [p3 p4]. move: p2 p4=> [q1 q2 q3] [q4 q5 q6]. move: p1 p3 => /functionsP [fu su tu] /functionsP[fv sv tv]. have cuv: composable u v by split => //; ue. have mv: inc m (source v) by ue. move: q1 =>[_ _ _ incf]; move: (incf _ _ (q5 _ ms)) => le1. move: (q2 _ ms) => le2. have ne: nonempty y. exists m; apply: Zo_i => //; split => //; rewrite compfV//; apply: mm; order_tac. apply: (wor _ sy ne). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)