proposition: Theorem sup_induced1 r A F: order r -> sub F (substrate r) -> sub A F -> has_supremum r A -> has_supremum (induced_order r F) A -> gle r (supremum r A) (supremum (induced_order r F) A).
proof: Proof. move=> or Fs AF sA siA. have [oi si]:= (iorder_osr or Fs). have As:sub A (substrate r) by apply: sub_trans Fs. have Asi: sub A (substrate (induced_order r F)) by ue. move: (supremum_pr1 or sA) (supremum_pr1 oi siA). set (u:= supremum r A). set (v:=supremum (induced_order r F) A). move=> /(lubP or As) [ub lub] /(lubP oi Asi) [[us ubi] lubi]; apply: lub. move: us; rewrite si=> vF. split;[ by apply: Fs | move=> y yA; move: (ubi _ yA); apply:iorder_gle1]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)