proposition: Lemma partition_less_imp_gt_zero : forall n (P : Partition Hab n), a [<] b -> 0 < n.
proof: Proof. intros n P H. cut (0 <> n); intro. apply Nat.neq_0_lt_0; auto. exfalso. cut (a [=] b). intro; apply less_irreflexive_unfolded with (x := a). astepr b; assumption. apply partition_length_zero. rewrite H0; apply P. Qed.
imports: CoRN.ftc.Continuity Coq(Lia)