add some lemmas about `Finite` and `pred_finite`

Merge it if you like it. Feel free to suggest better naming and placement.

added 1 commit

• e36e6bd9 - add some lemmas about `Finite` and `pred_finite`

Compare with previous version

resolved all threads

added 1 commit

• ffacf118 - clean some statements and improve formatting of one proof

Compare with previous version

added 1 commit

• 97c7a0ec - shorten the proof of `dec_pred_finite`

Compare with previous version

added 4 commits

• 2f38c91e - clean some statements and improve formatting of one proof
• 719a03c0 - shorten the proof of `dec_pred_finite`
• 0a5ee6f8 - remove lemma `finite_dec`
• 804d5042 - comment about `dec_pred_finite_alt` and prove related lemmas

Compare with previous version

added 1 commit

• e06129b0 - comment about `dec_pred_finite_alt` and prove related lemmas

Compare with previous version

added 1 commit

• 35d5600f - simplify proof of `finite_sig_dec`, remove lemmas about `pred_finite_alt`

Compare with previous version

added 1 commit

• d95046c3 - add comment about Qed/Defined for `finite_sig_dec`

Compare with previous version