proposition: Lemma expr_compare_spec n m (x y: expr n m): compare_spec (x=y) (expr_compare x y).
proof: Proof. generalize (fun H => expr_compare_eq_dep x y H eq_refl eq_refl) as H. generalize (@expr_compare_eq _ _ x y) as H'. case (expr_compare x y); intros H' H; constructor. now apply cmp_eq_dep_eq in H. intro E. now discriminate H'. intro E. now discriminate H'. Qed.
imports: positives comparisons Eqdep monoid