fact: Definition triangle k i := match k with | 1 => i | k'~0 => k'*Pdouble_minus_one k'+i | k'~1 => k'*k+i end.
imports: ATBR(Common) ATBR(BoolView) ATBR(MyFSets MyFSetProperties MyFMapProperties) Coq(FSetPositive FMapPositive)