proposition: Lemma lattice_props: ( (forall x y, inc x E-> inc y E -> inc (sup r x y) E) /\ (forall x y, inc x E-> inc y E -> inc (inf r x y) E) /\ (forall x y, inc x E-> inc y E -> sup r (inf r x y) y = y) /\ (forall x y, inc x E-> inc y E -> inf r (sup r x y) y = y) /\ (forall x y z, inc x E-> inc y E -> inc z E -> sup r x (sup r y z) = sup r (sup r x y) z) /\ (forall x y z, inc x E-> inc y E -> inc z E -> inf r x (inf r y z) = inf r (inf r x y) z) /\ (forall x, inc x E -> sup r x x = x) /\ (forall x, inc x E -> inf r x x = x) /\ (forall x y, inc x E-> inc y E -> sup r (sup r x y) x = sup r x y) /\ (forall x y, inc x E-> inc y E -> inf r (inf r x y) x = inf r x y) ).
proof: Proof. move: (lr) => [or _]. have sa:(forall x y z, inc x E-> inc y E -> inc z E -> sup r x (sup r y z) = sup r (sup r x y) z). move => x y z xE yE zE. have [le1 le2 le3] := (lattice_sup_pr lr xE yE). have [le4 le5 le6] := (lattice_sup_pr lr yE zE). have s1r: (inc (sup r y z) (substrate r)) by order_tac. have s2r: (inc (sup r x y) (substrate r)) by order_tac. have [le1' le2' le3'] := (lattice_sup_pr lr xE s1r). have [le4' le5' le6'] := (lattice_sup_pr lr s2r zE). apply: (order_antisymmetry or). apply: le3'. apply: (order_transitivity or le1 le4'). apply: le6 => //; apply: (order_transitivity or le2 le4'). apply: le6'. apply: le3 => //. apply: (order_transitivity or le4 le2'). apply: (order_transitivity or le5 le2'). have ia: (forall x y z, inc x E-> inc y E -> inc z E -> inf r x (inf r y z) = inf r (inf r x y) z). move => x y z xE yE zE. have [le1 le2 le3] := (lattice_inf_pr lr xE yE). have [le4 le5 le6] := (lattice_inf_pr lr yE zE). have s1r: (inc (inf r y z) (substrate r)) by order_tac. have s2r: (inc (inf r x y) (substrate r)) by order_tac. have [le1' le2' le3'] := (lattice_inf_pr lr xE s1r). have [le4' le5' le6']:= (lattice_inf_pr lr s2r zE). apply: (order_antisymmetry or). apply: le6'. apply: le3 => //. apply: (order_transitivity or le2' le4). apply: (order_transitivity or le2' le5). apply: le3'. apply: (order_transitivity or le4' le1). apply: le6 => //; apply: (order_transitivity or le4' le2). have sxx:forall x, inc x E -> sup r x x = x. by move => x xE; apply: sup_comparable1 => //; order_tac. have ixx:forall x, inc x E -> inf r x x = x. by move => x xE; apply: inf_comparable1 => //; order_tac. split. move => x y xE yE; move: (lattice_sup_pr lr xE yE) => [le1 e2 le3]. rewrite /E;order_tac. split. move => x y xE yE; move: (lattice_inf_pr lr xE yE) => [le1 le2 le3]. rewrite /E;order_tac. split. move => x y xE yE; move: (lattice_inf_pr lr xE yE) => [le1 le2 le3]. apply: (sup_comparable1 or le2). split. move => x y xE yE; move: (lattice_sup_pr lr xE yE) => [le1 le2 le3]. rewrite inf_C; apply: (inf_comparable1 or le2). split; [ exact | split; [exact | split ; [exact | split => //]]]. split. by move => x y xE yE; rewrite sup_C sa // sxx. by move => x y xE yE; rewrite inf_C ia // ixx. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)