proposition: Theorem and_assoc : forall P Q R : Prop, P /\ (Q /\ R) -> (P /\ Q) /\ R.
proof: Proof. MProof. pintros \P Q R [| \HP [| \HQ HR]]. Admitted. Check and. Lemma or_example : forall n m : nat, n = 0 \/ m = 0 -> n * m = 0. MProof. pintros \n m [| \Hn | \Hm]. - rewrite Hn. reflexivity. - rewrite Hm. rewrite <- mult_n_O. reflexivity. Qed.