fact: Fixpoint mult (a b : t) : t := match a, b with | nil, _ => zero | _, nil => zero | cons 0 n _, cons 0 n' b' => cons 0 (Peano.pred((S n) * (S n'))) b' | cons a n b, cons 0 n' _ => cons a (Peano.pred ((S n) * (S n'))) b | cons a n b, cons a' n' b' => cons (a + a')%nat n' ((cons a n b) * b') end where "a * b" := (mult a b) : lo_scope.
imports: hydras(T1 E0 Comparable) Coq(Arith Logic.Eqdep_dec Peano_dec List Bool Recdef Lia Wellfounded.Inverse_Image Wellfounded.Inclusion RelationClasses )