proposition: Lemma compat_prd_unit_add : forall x h, compat_prd_unit h -> compat_prd_unit (add_to_prd i is_unit x h).
proof: Proof. intros; unfold add_to_prd, comp. case (is_prd_spec); intros; try constructor; auto. - unfold comp; case h; try constructor. - unfold comp; case h; try constructor. Qed.
imports: Coq(Arith NArith List) Coq(FMapPositive Relations RelationClasses) AAC_tactics(Utils Constants)