proposition: Lemma compare_reflect : forall alpha beta, match compare alpha beta with | Lt => lt alpha beta | Eq => alpha = beta | Gt => lt beta alpha end.
proof: Proof. unfold lt; induction alpha, beta. 1-3: easy. specialize (IHalpha1 beta1). specialize (IHalpha2 beta2). rewrite !compare_cons. rewrite compare_rev with alpha1 beta1, compare_rev with alpha2 beta2, Nat.compare_antisym in *. destruct (compare alpha1 beta1), (compare alpha2 beta2), (n0 ?= n) eqn:Heq; simpl in *; subst. 2-27: easy. now apply Nat.compare_eq_iff in Heq as ->. Qed.
imports: Coq(Arith Max Bool Lia Compare_dec Relations Ensembles Wellfounded Bool RelationClasses Operators_Properties ArithRing Logic.Eqdep_dec) hydras(More_Arith Restriction DecPreOrder) hydras(OrdNotations)