fact: Fixpoint expr_compare (x y: expr A) := match x,y with | e_bot, e_bot | e_top, e_top => Eq | e_var a, e_var b => cmp a b | e_cup x x', e_cup y y' | e_cap x x', e_cap y y' => lex (expr_compare x y) (expr_compare x' y') | e_neg x, e_neg y => expr_compare x y | e_bot, _ => Lt | _, e_bot => Gt | e_top, _ => Lt | _, e_top => Gt | e_var _, _ => Lt | _, e_var _ => Gt | e_cup _ _, _ => Lt | _, e_cup _ _ => Gt | e_cap _ _, _ => Lt | _, e_cap _ _ => Gt end.
imports: positives comparisons lattice lset sups