fact: Fixpoint nat_double_rec (n m:nat){struct n} : P n m := match n, m return P n m with | 0 , x => base_case1 x | (S x), 0 => base_case2 x | (S x), (S y) => inductive_step x y (nat_double_rec x y) end.
imports: Arith Vector List Extraction ZArith Compare_dec ZArith List