fact: Fixpoint axp_scheme {A} p : A -> A -> @computation A := match p with | xH => (fun a x => y <--- a times x ; Return y) | xO q => (fun a x => x2 <--- x times x ; axp_scheme q a x2) | xI q => (fun a x => ax <--- a times x ; x2 <--- x times x ; axp_scheme q ax x2) end.
imports: Coq(Relations RelationClasses Lia List) Param(Param) additions(More_on_positive)