proposition: Lemma downK A : down (down A) = down A.
proof: Proof. rewrite predeqE => x; split; last by move=> Ax; apply/downP; exists x. case/downP => y /downP[z Az yz xy]. by apply/downP; exists z => //; rewrite (le_trans xy). Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra) mathcomp(mathcomp_extra boolp classical_sets set_interval) Setoid