proposition: Lemma compare_rev : forall (alpha beta : T1), compare beta alpha = CompOpp (compare alpha beta).
proof: Proof. induction alpha, beta. 1-3: easy. rewrite !compare_cons. rewrite IHalpha1, Nat.compare_antisym. destruct (compare alpha1 beta1); simpl. 2-3: easy. now destruct (n ?= n0) eqn:?; simpl. 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)