proposition: Lemma CRadd_eq_compat : forall a b c d, a == c -> b == d -> a + b == c + d.
proof: Proof. intros ? ? ? ? H H'. rewrite H; rewrite H'. ring. Qed.
imports: Type_class_definition Type_class_instance Coq.Relations.Relation_Definitions Lia Arith Nbinomial Setoid