proposition: Remark Rem08 : (0 <= l)%nat /\ (l < t)%nat /\ (forall i : nat, (0 <= i)%nat -> (i <= l)%nat -> P i) /\ ~ P (S l).
proof: Proof. unfold l; pattern (proj1_sig l_def); apply proj2_sig. Qed.
imports: hydras(DecPreOrder Canon MoreLists First_toggle OrdNotations) Coq(Lia)