proposition: Lemma expr_compare_eq n m (x y: expr n m): x=y -> expr_compare x y = Eq.
proof: Proof. intros <-. induction x; simpl expr_compare; trivial; rewrite ?compare_lex_eq, ?cmp_refl; tauto. Qed.
imports: positives comparisons Eqdep monoid