proposition: Lemma compare_rev : forall (a b : t), compare b a = CompOpp (compare a b).
proof: Proof. induction a, b. - easy. - cbn; destruct p; cbn; trivial. - cbn; destruct a; reflexivity. - cbn; rewrite IHa. destruct p, a; rewrite Nat.compare_antisym. destruct (Nat.compare n1 n) eqn:? ; cbn; trivial. rewrite Nat.compare_antisym; destruct (Nat.compare n2 n0) eqn:? ; now cbn. Qed.
imports: hydras(T1 E0 Comparable) Coq(Arith Logic.Eqdep_dec Peano_dec List Bool Recdef Lia Wellfounded.Inverse_Image Wellfounded.Inclusion RelationClasses )