proposition: Lemma Zlt_reg_l : forall a b c : Z, (a < b)%Z -> (c + a < c + b)%Z.
proof: Proof. intros a b c; try assumption. unfold Zlt, not in |- *. intros H'; try assumption. rewrite <- H'. apply Zcompare_plus_compat; assumption. Qed.
imports: Zring Group_kernel