proposition: Lemma sublattice_pr r A (rA:= induced_order r A): lattice r -> sublattice r A -> sub A (substrate r)-> [/\ lattice rA, substrate rA = A, (forall a b, inc a A -> inc b A -> sup r a b = sup rA a b) & (forall a b, inc a A -> inc b A -> inf r a b = inf rA a b) ].
proof: Proof. move => lr sla sa. move: (lr) => [or lr1]. move: (iorder_osr or sa) => [orA srA]. have auxP: forall a b, inc a A -> inc b A -> (gle rA a b <-> gle r a b). move => a b aA bA; exact :(iorder_gle0P _ aA bA). have pa: forall a b, inc a A -> inc b A -> (least_upper_bound rA (doubleton a b) (sup r a b) /\ greatest_lower_bound rA (doubleton a b) (inf r a b)). move => a b aA bA. have da: sub (doubleton a b) (substrate rA). by move => t /set2_P [] ->; rewrite srA. move: (lr1 _ _ (sa _ aA) (sa _ bA)) => [ta tb]. move: (sup_pr or (sa _ aA) (sa _ bA) ta) => [s1 s2 s3]. move: (inf_pr or (sa _ aA) (sa _ bA) tb) => [s4 s5 s6]. move: (sla _ _ aA bA)=> [s7 s8]; split. apply /(lubP orA da); rewrite /upper_bound srA;split => //. by split => //;move => y /set2_P [] ->; apply /auxP. move => z [zA sz]; apply /auxP => //; apply: s3; apply /auxP=> //; apply: sz; fprops. apply /(glbP orA da); rewrite /lower_bound srA;split => //. by split => //;move => y /set2_P [] ->; apply /auxP. move => z [zA sz]; apply /auxP=> //; apply: s6; apply /auxP => //; apply: sz; fprops. split => //. + split; first by exact. rewrite srA; move => x y xA yA; move: (pa _ _ xA yA)=> [qa qb]. split; [ by exists (sup r x y) | by exists (inf r x y)]. + move => x y xA yA; move: (pa _ _ xA yA)=> [qa qb]. exact (supremum_pr2 orA qa). + move => x y xA yA; move: (pa _ _ xA yA)=> [qa qb]. exact (infimum_pr2 orA qb). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)