Switched to the algorithmically improved implementation

is_redblackP lemma admitted for the moment