induction a using (repeat_while_smaller_ind A size)

Update README.md

add version using Equations package

next idea: generic repeat_while_smaller

use ssreflect, prove f3_not_even_id

next idea: repeat until local minimum

f2_id using def_f2

WfExtensionality.unfold_sub

update .gitignore

add about-program-fixpoint.v

.txt

Initial commit