proposition: Lemma Exercise1_17b r: boolean_lattice r -> order_isomorphism (Lf (standard_completion r) (substrate r)(substrate r)) r (opp_order r).
proof: Proof. move=> blr. have ta: (lf_axiom (standard_completion r) (substrate r) (substrate r)). by move=> t tsr; move: (scompl_pr blr tsr) => [ok _]. move: (blr) => [[[or _] _ _ ] _ _]. move: (opp_osr or) => [pa pb]. split => //. saw; try ue; apply: lf_bijective =>//. move=> u v uE vE ss; rewrite -(scomplI blr uE) -(scomplI blr vE) ss //. by move => u uE; move: (ta _ uE) => h; ex_tac; rewrite (scomplI blr uE). red; aw;move=> x y xE yE; rewrite !LfV//; split. by move => h; apply /opp_gleP; apply: scompl_mon. move /opp_gleP; rewrite -{2} (scomplI blr xE) -{2} (scomplI blr yE). by apply: scompl_mon. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)