fact: Fixpoint expr_compare n m (x: expr n m) p q (y: expr p q) := match x,y with | e_zer _ _, e_zer _ _ | e_top _ _, e_top _ _ | e_one _, e_one _ => Eq | e_var a, e_var b => cmp a b | e_pls _ _ x x', e_pls _ _ y y' | e_cap _ _ x x', e_cap _ _ y y' => lex (expr_compare x y) (expr_compare x' y') | e_dot _ u _ x x', e_dot _ v _ y y' | e_ldv u _ _ x x', e_ldv v _ _ y y' | e_rdv u _ _ x x', e_rdv v _ _ y y' => lex (cmp u v) (lex (expr_compare x y) (expr_compare x' y')) | e_neg _ _ x, e_neg _ _ y | e_itr _ x, e_itr _ y | e_str _ x, e_str _ y | e_cnv _ _ x, e_cnv _ _ y => expr_compare x y | e_zer _ _, _ => Lt | _, e_zer _ _ => Gt | e_one _, _ => Lt | _, e_one _ => Gt | e_top _ _, _ => Lt | _, e_top _ _ => Gt | e_var _, _ => Lt | _, e_var _ => Gt | e_itr _ _, _ => Lt | _, e_itr _ _ => Gt | e_str _ _, _ => Lt | _, e_str _ _ => Gt | e_cnv _ _ _, _ => Lt | _, e_cnv _ _ _ => Gt | e_ldv _ _ _ _ _, _ => Lt | _, e_ldv _ _ _ _ _ => Gt | e_rdv _ _ _ _ _, _ => Lt | _, e_rdv _ _ _ _ _ => Gt | e_pls _ _ _ _, _ => Lt | _, e_pls _ _ _ _ => Gt | e_cap _ _ _ _, _ => Lt | _, e_cap _ _ _ _ => Gt | e_neg _ _ _, _ => Lt | _, e_neg _ _ _ => Gt end.
imports: positives comparisons Eqdep monoid