proposition: Theorem lexico_anti_sym: forall a b, lexico b a = opp (lexico a b).
proof: Proof. intros a; elim a; clear a; simpl; auto. intros b; case b; clear b; simpl; auto. intros x a Rec b; case b; clear b; simpl; auto. intros y b; rewrite (weight_anti_sym x y). case (weight x y); simpl; auto. Qed.
imports: List Permutation UList