proposition: Lemma o_size2_trans : transitive _ o_size2.
proof: Proof. intros [x1 x2] [y1 y2] [z1 z2]. apply (lex_trans Nat.eqb beq_nat_ok). intros n m n_lt_m m_lt_n; generalize (Nat.lt_asymm n m n_lt_m m_lt_n); contradiction. intros n1 n2 n3; apply Nat.lt_trans. intros n1 n2 n3; apply Nat.lt_trans. Qed.
imports: Coq(Bool Peano List PeanoNat) CoLoR(closure more_list equiv_list list_permut dickson) Coq(Relations Wellfounded Arith Wf_nat Recdef Program Morphisms Lia) CoLoR(term_spec term decidable_set ordered_set NatCompat)