proposition: Lemma compare_fin_rw (n n1: nat) : compare (T1nat n) (T1nat n1) = (n ?= n1).
proof: Proof. destruct n, n1. - easy. - now cbn. - now cbn. - cbn; unfold compare; case (n ?= n1); trivial. 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)