proposition: Lemma add_0_r : forall x:nat, x + 0 =N= x.
proof: Proof. intros a;induction a as [|a IH]. + reflexivity. + apply (ap S),IH. Qed.
imports: HoTT.Classes.interfaces.abstract_algebra HoTT.Classes.interfaces.naturals HoTT.Classes.interfaces.orders HoTT.Classes.theory.rings HoTT.Classes.orders.semirings HoTT.Classes.theory.apartness