proposition: Theorem lexico_trans: forall a b c, lexico a b = lexico b c -> lexico a c = lexico a b.
proof: Proof. intros a; elim a; simpl; auto; clear a. intros b; case b; auto; clear b. intros x b c; case c; clear c; simpl; auto. intros; discriminate. intros x a Rec; intros b c; case c; case b; clear b c; simpl; try (intros; discriminate; fail); auto. intros y b z c. case_eq (weight x y); auto; intros H1. case_eq (weight y z); auto; intros H2. rewrite (weight_trans x y z); rewrite H1; auto. rewrite <- (weight_compat_r y z x); auto. rewrite H1; auto. intros; discriminate. rewrite (weight_compat_l x y z); auto. case_eq (weight y z); auto; intros H2. case_eq (weight y z); auto; intros H2. intros; discriminate. rewrite <- (weight_compat_r y z x); auto. rewrite H1; auto. rewrite (weight_trans x y z); auto. rewrite H1; auto. rewrite H1; auto. Qed.
imports: List Permutation UList