proposition: Lemma ex6_fct_bp: bijection_prop ex6_iso (inductive_limit ex6_F) (inductive_limit S).
proof: Proof. rewrite/ex6_iso; split; aw;split; [ apply: ex6_fct_fi | apply: ex6_fct_fs]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)