Description: Schema for strong induction on the cardinality of a finite set. The inductive hypothesis is that the result is true on any proper subset. The result is then proven to be true for all finite sets. (Contributed by Mario Carneiro, 13-Dec-2013)
Ref | Expression | ||
---|---|---|---|
Hypotheses | findcard3.1 | |
|
findcard3.2 | |
||
findcard3.3 | |
||
Assertion | findcard3 | |