proposition: Lemma o_size3_trans : transitive _ o_size3.
proof: Proof. generalize (lex_trans _ _ eq_nat_dec lt (lex _ _ eq_nat_dec lt lt)); unfold transitive, o_size3, size3, o_size2; intros H x y z lt1 lt2; destruct x; destruct p; rename t into x1; rename t0 into x2; rename t1 into x3; destruct y; destruct p; rename t into y1; rename t0 into y2; rename t1 into y3; destruct z; destruct p; rename t into z1; rename t0 into z2; rename z1 into z3. apply H with (size y1, size2 (y2,y3)); trivial. unfold antisymmetric; intros n m lt' lt''; generalize (lt_asym n m lt' lt''); contradiction. apply lt_trans. fold transitive; apply lex_trans. unfold antisymmetric; intros n m lt' lt''; generalize (lt_asym n m lt' lt''); contradiction. unfold transitive; apply lt_trans. unfold transitive; apply lt_trans. Qed.
imports: List more_list list_permut dickson Relations Wellfounded Arith Wf_nat term