proposition: Theorem weight_compat_r: forall a b c, weight a b = eq -> weight c a = weight c b.
proof: Proof. intros a b c H; repeat rewrite (fun x => weight_anti_sym x c). rewrite weight_compat_l with (b := b); auto. Qed.
imports: List Permutation UList