proposition: Lemma perm_intro_r : forall l1 l2 :list A, perm l1 l2 -> forall l, transpose l l1 -> perm l l2.
proof: Proof. induction 1. - intros l H; constructor 2 with l; [left | assumption]. - intros l Hl; constructor 2 with l';auto. Qed.
imports: List Relations