fact: Definition sum_no_zero n := let: P := (fun n => if n is 0 then unit else nat) in nat_rec P tt (fun n' m => match n' return P n' -> _ with | 0 => fun _ => 1 | n''.+1 => fun m => my_plus m (n'.+1) end m) n.
imports: mathcomp(ssreflect ssrbool) mathcomp(ssrnat)