proposition: Lemma list_compare_trans : SymTrans cmp -> Trans list_compare.
proof: Proof. intros HA c. induction x as [|a x IH]; destruct y as [|a' y], z as [|a'' z]; simpl; auto; try congruence. destruct (cmp a a') eqn:E, (cmp a' a'') eqn:E'; simpl; try congruence. - rewrite tra; eauto. simpl; eauto. - intros _ <-. rewrite SymTrans_CompatL, E'; eauto. - intros _ <-. rewrite SymTrans_CompatL, E'; eauto. - intros <- _. rewrite SymTrans_CompatR, E; eauto. now flipcmp E'. - intros <- _. rewrite tra; eauto. easy. - intros <- _. rewrite SymTrans_CompatR, E; eauto. now flipcmp E'. - intros <- _. rewrite tra; eauto. easy. Qed.
imports: Coq(List)