fact: Example C7 : chain := fun (A:Type) (x:A) => x2 <--- x times x; x3 <--- x2 times x; x6 <--- x3 times x3 ; x7 <--- x6 times x; Return x7.
imports: Coq(Relations RelationClasses Lia List) Param(Param) additions(More_on_positive)