Formalization of the online matching algorithm RANKING introduced by Karp, Vazirani, and Vazirani [1], following the proof by Birnbaum, and Mathieu [2].
[1] Karp, Richard M., Umesh V. Vazirani, and Vijay V. Vazirani. "An optimal algorithm for on-line bipartite matching." Proceedings of the twenty-second annual ACM symposium on Theory of computing. 1990.
[2] Birnbaum, Benjamin, and Claire Mathieu. "On-line bipartite matching made simple." Acm Sigact News 39.1 (2008): 80-87.