proposition: Lemma add_diag n : n + n = 2 * n.
proof: Proof. change 2 with (1+1). now rewrite mul_add_distr_r, !mul_1_l. Qed.
imports: BinNums BinPos Pnat BinNat Bool Equalities GenericMinMax OrdersFacts ZAxioms ZProperties DecidableClass