proposition: Fact pair_add0 : left_id (0, 0) add_pair.
proof: Proof. by case=> x1 x2; congr (_, _); apply: add0r. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq) mathcomp(choice fintype finfun bigop prime binomial)