proposition: Lemma repeat_nat_pos : forall n, 0 < Core.nat_iter (S n) (plus 1) 0.
proof: Proof. intros n. simpl. apply pos_plus_le_lt_compat_l. - solve_propholds. - apply repeat_nat_nonneg. Qed.
imports: HoTT.Classes.theory.apartness HoTT.Classes.interfaces.abstract_algebra HoTT.Classes.interfaces.orders HoTT.Classes.theory.rings HoTT.Classes.orders.orders HoTT.Classes.orders.maps