fact: Fixpoint shiftl_aux p cont x n := shiftl_aux_body (fun x n => match p with | xH => cont x n | xO p => shiftl_aux p (shiftl_aux p cont) x n | xI p => shiftl_aux p (shiftl_aux p cont) x n end) x n.
imports: Bool BigNumPrelude ZArith Lia Nnat Ndigits CyclicAxioms DoubleType Nbasic Wf_nat StreamMemo NSig NMake_gen