intros.simplify.left.apply le_O_n.
intros.simplify.right.exact not_le_Sn_O n1.
intros 2.simplify.intro.elim H.
left.apply le_S_S.assumption.
right.intro.apply H1.apply le_S_S_to_le.assumption.
qed.
intros.simplify.left.apply le_O_n.
intros.simplify.right.exact not_le_Sn_O n1.
intros 2.simplify.intro.elim H.
left.apply le_S_S.assumption.
right.intro.apply H1.apply le_S_S_to_le.assumption.
qed.