proposition: Lemma sublattice_dr r A : lattice r -> sublattice r A -> sub A (substrate r)-> distributive_lattice1 r -> distributive_lattice3 (induced_order r A).
proof: Proof. move=> lr slr sard dl1. move: (sublattice_pr lr slr sard) => [lA srA sA iA]. have pa: distributive_lattice1 (induced_order r A). move => x y z; rewrite srA => xA yA zA. rewrite - (sA _ _ xA zA) - (sA _ _ xA yA) - (iA _ _ yA zA). move:(proj1 (slr _ _ xA yA)) (proj1 (slr _ _ xA zA)) => xyA xzA. rewrite - (iA _ _ (proj1 (slr _ _ xA yA)) (proj1 (slr _ _ xA zA))). rewrite - (sA _ _ xA (proj2 (slr _ _ yA zA))). exact (dl1 _ _ _ (sard _ xA)(sard _ yA)(sard _ zA)). exact (proj1 (distributive_lattice_prop1 lA) pa). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)