fact: Fixpoint T1mul (c1 c2 : T1) {struct c2}:T1 := if c2 is cons a' n' b' then if c1 is cons a n b then if((a==zero) && (a' == zero)) then cons zero (n*n' + n + n')%N b' else if(a'==zero) then cons a (n*n' + n + n')%N b else cons (a + a') n' ((cons a n b) * b') else zero else zero where "c1 * c2" := (T1mul c1 c2) : cantor_scope.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)