fact: Fixpoint computation_length {A} (a:A) (m : @computation A) : nat := match m with | Mult _ _ k => S (computation_length a (k a)) | _ => 0%nat end.
imports: Coq(Relations RelationClasses Lia List) Param(Param) additions(More_on_positive)