proposition: Lemma distrib_r_of_comm_distrib_l : forall f g, comm f -> distrib_l f g -> distrib_r f g.
proof: Proof. Proof using. introv C N. intros_all. unfolds distrib_l. do 3 rewrite <- (C x). auto. Qed.
imports: TLC(LibTactics)