p q : p * q = q * p. Proof. induction q; simpl. 1: apply pos_mul_1_r. + rewrite mul_xO_r. f_ap. + rewrite mul_xI_r. f_ap; f_ap. Qed.
Require Import Basics.Overture Basics.Tactics. Require Import Pos.Core.