fact: Definition binary_rect (P:N -> Type) (f0 : P 0) (f2 : forall n, P n -> P (double n)) (fS2 : forall n, P n -> P (succ_double n)) (n : N) : P n := let P' p := P (pos p) in let f2' p := f2 (pos p) in let fS2' p := fS2 (pos p) in match n with | 0 => f0 | pos p => positive_rect P' fS2' f2' (fS2 0 f0) p end.
imports: BinNums BinPos RelationClasses Morphisms Setoid Equalities OrdersFacts GenericMinMax Bool NAxioms NMaxMin NProperties