take seq_const 1 ; :: thesis: seq_const 1 is nonnegative-yielding
thus seq_const 1 is nonnegative-yielding ; :: thesis: verum