proposition: Lemma double2 A (x: A) f t: t = double f x -> double f t = nat_iter 4 f x.
proof: Proof. move=>Et; rewrite Et. rewrite /double /nat_iter. Restart. by move=>->. Qed.
imports: mathcomp(ssreflect ssrfun eqtype ssrnat ssrbool)