Welcome to your own jsCoq development

Want to create a document like this one? Copy node_modules/jscoq/examples/npm-template.html and start editing.

From elpi Require Import elpi. From HB Require Import structures. From mathcomp Require Import all_ssreflect. HB.about Equality.type. From mathcomp Require Import all_algebra ring. Import GRing.Theory. Open Scope ring_scope. Section AbstractCommutativeRing. Variables (R : comRingType) (a b c : R). Goal a + b + c = a + c + b. Proof. ring. Qed. End AbstractCommutativeRing.