proposition: Lemma and_or_distrib_left (P Q R : Prop) : P ∧ (Q ∨ R) ↔ (P ∧ Q) ∨ (P ∧ R).
proof: Proof. split. intro f. destruct f as [p qr]. destruct qr as [q|r]. left. split; assumption. right. split; assumption. intro f. destruct f as [pq|pr]. destruct pq as [p q]. split. exact p. left. exact q. destruct pr as [p r]. split. exact p. right. exact r. Qed.
imports: Unicode.Utf8 Classical