proposition: Lemma size_fact_seq n : size (fact_seq n) = n.+1.
proof: Proof. by rewrite size_rec1up. Qed.
imports: Coq(ZArith Rfunctions NaryFunctions Lia) mathcomp.ssreflect(ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop tuple) MathComp