Hola.
Incluyo la prueba del primer lema para que veas aplicaciones de los axiomas referidos (en particular de sumS, según lo mencionás). La prueba del lema 10_5 te la dejo a vos (es un poco más larga).
Lemma L10_4: forall m n: nat, n <> O -> sum m n <> O.
Proof.
unfold not; intros m n H1 H2.
elim (allNat n); intro H3. (* notar que sum analiza casos para el segundo argumento: n *)
apply H1; assumption.
elim H3; intros x H4. (* en el caso del existe es necesario usar/obtener información de éste *)
rewrite <- H4 in H2.
rewrite sumS in H2. (* acá uso sumS *)
symmetry in H2. (* la igualdad está al revés para poder usar disc *)
apply (disc (sum m x)); assumption. (* y acá disc *)
Qed.
Saludos, Carlos