a b : S a + b =N= S (a + b) := idpath. Local Instance add_0_r : RightIdentity@{N N} (plus : Plus nat) (zero : Zero nat). Proof. intros a; induction a as [| a IHa]. - reflexivity. - apply (ap S), IHa. Qed.
Require Import